Tue, 09 Dec 2008 15:31:38 -0800 |
huffman |
move lemmas from Numeral_Type.thy to other theories
|
file |
diff |
annotate
|
Wed, 19 Nov 2008 17:54:55 +0100 |
nipkow |
Added new fold operator and renamed the old oe to fold_image.
|
file |
diff |
annotate
|
Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
Sun, 24 Aug 2008 14:42:22 +0200 |
haftmann |
tuned import order
|
file |
diff |
annotate
|
Tue, 15 Jul 2008 16:50:09 +0200 |
ballarin |
Removed uses of context element includes.
|
file |
diff |
annotate
|
Tue, 01 Jul 2008 20:26:48 +0200 |
huffman |
prove lemma finite in context of finite class
|
file |
diff |
annotate
|
Tue, 01 Jul 2008 06:51:59 +0200 |
huffman |
remove simp attribute from range_composition
|
file |
diff |
annotate
|
Thu, 12 Jun 2008 14:10:41 +0200 |
nipkow |
Hid swap
|
file |
diff |
annotate
|
Wed, 07 May 2008 10:56:34 +0200 |
berghofe |
- Deleted code setup for finite and card
|
file |
diff |
annotate
|
Mon, 28 Apr 2008 20:21:11 +0200 |
haftmann |
thms Max_ge, Min_le: dropped superfluous premise
|
file |
diff |
annotate
|
Fri, 25 Apr 2008 15:30:33 +0200 |
krauss |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
file |
diff |
annotate
|
Fri, 28 Mar 2008 22:00:59 +0100 |
haftmann |
only invoke interpret
|
file |
diff |
annotate
|
Thu, 27 Mar 2008 19:04:35 +0100 |
haftmann |
no "attach UNIV" any more
|
file |
diff |
annotate
|
Tue, 26 Feb 2008 20:38:10 +0100 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
Wed, 06 Feb 2008 08:34:32 +0100 |
haftmann |
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
|
file |
diff |
annotate
|
Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
Thu, 29 Nov 2007 17:08:26 +0100 |
haftmann |
instance command as rudimentary class target
|
file |
diff |
annotate
|
Fri, 23 Nov 2007 21:09:32 +0100 |
haftmann |
deleted card definition as code lemma; authentic syntax for card
|
file |
diff |
annotate
|
Tue, 06 Nov 2007 08:47:25 +0100 |
haftmann |
renamed lordered_*_* to lordered_*_add_*; further localization
|
file |
diff |
annotate
|
Fri, 26 Oct 2007 21:22:16 +0200 |
haftmann |
dropped "brown" syntax
|
file |
diff |
annotate
|
Tue, 23 Oct 2007 23:27:23 +0200 |
nipkow |
went back to >0
|
file |
diff |
annotate
|
Tue, 16 Oct 2007 23:12:45 +0200 |
haftmann |
global class syntax
|
file |
diff |
annotate
|
Mon, 15 Oct 2007 15:29:39 +0200 |
haftmann |
explicit parameter for class finite
|
file |
diff |
annotate
|
Mon, 08 Oct 2007 08:04:26 +0200 |
haftmann |
clarified
|
file |
diff |
annotate
|
Fri, 05 Oct 2007 08:38:09 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
Sat, 29 Sep 2007 08:58:51 +0200 |
haftmann |
proper syntax during class specification
|
file |
diff |
annotate
|
Wed, 26 Sep 2007 20:27:55 +0200 |
haftmann |
moved Finite_Set before Datatype
|
file |
diff |
annotate
|
Thu, 20 Sep 2007 16:37:28 +0200 |
haftmann |
code lemmas for cardinality
|
file |
diff |
annotate
|
Sat, 15 Sep 2007 19:27:41 +0200 |
haftmann |
added lemmas for finiteness
|
file |
diff |
annotate
|
Fri, 24 Aug 2007 14:21:33 +0200 |
paulson |
revised blacklisting for ATP linkup
|
file |
diff |
annotate
|