Tue, 10 Jul 2007 17:30:45 +0200 |
haftmann |
moved some finite lemmas here
|
file |
diff |
annotate
|
Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
Sun, 17 Jun 2007 18:47:03 +0200 |
nipkow |
tuned laws for cancellation in divisions for fields.
|
file |
diff |
annotate
|
Fri, 15 Jun 2007 15:10:32 +0200 |
nipkow |
made divide_self a simp rule
|
file |
diff |
annotate
|
Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
Wed, 06 Jun 2007 17:01:33 +0200 |
huffman |
generalize class constraints on some lemmas
|
file |
diff |
annotate
|
Mon, 04 Jun 2007 15:43:30 +0200 |
haftmann |
tuned comments
|
file |
diff |
annotate
|
Thu, 24 May 2007 08:37:39 +0200 |
haftmann |
rudimentary class target implementation
|
file |
diff |
annotate
|
Sat, 19 May 2007 11:33:22 +0200 |
haftmann |
no special treatment in naming of locale predicates stemming form classes
|
file |
diff |
annotate
|
Fri, 11 May 2007 20:47:30 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
Fri, 11 May 2007 03:31:12 +0200 |
huffman |
generalize setsum lemmas from semiring_0_cancel to semiring_0
|
file |
diff |
annotate
|
Thu, 10 May 2007 10:21:46 +0200 |
haftmann |
localized Min/Max
|
file |
diff |
annotate
|
Mon, 09 Apr 2007 21:28:24 +0200 |
huffman |
generalized type of lemma setsum_product
|
file |
diff |
annotate
|
Tue, 20 Mar 2007 08:27:15 +0100 |
haftmann |
explizit "type" superclass
|
file |
diff |
annotate
|
Fri, 16 Mar 2007 21:32:07 +0100 |
haftmann |
added FIXME hints
|
file |
diff |
annotate
|
Fri, 09 Mar 2007 08:45:57 +0100 |
haftmann |
moved order on functions here
|
file |
diff |
annotate
|
Sat, 03 Mar 2007 09:26:58 +0100 |
haftmann |
moved instance option :: finite here
|
file |
diff |
annotate
|
Fri, 02 Mar 2007 15:43:19 +0100 |
haftmann |
added code theorems for UNIV
|
file |
diff |
annotate
|
Wed, 14 Feb 2007 10:06:12 +0100 |
haftmann |
added class "preorder"
|
file |
diff |
annotate
|
Wed, 07 Feb 2007 17:28:09 +0100 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
Sun, 10 Dec 2006 07:12:26 +0100 |
nipkow |
Modified lattice locale
|
file |
diff |
annotate
|
Sat, 02 Dec 2006 11:33:08 +0100 |
haftmann |
generalized type signature of foldSet, fold
|
file |
diff |
annotate
|
Wed, 29 Nov 2006 04:11:06 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Sat, 18 Nov 2006 00:20:16 +0100 |
haftmann |
clarified module dependencies
|
file |
diff |
annotate
|
Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
Wed, 08 Nov 2006 19:48:34 +0100 |
haftmann |
renamed Lattice_Locales to Lattices
|
file |
diff |
annotate
|
Tue, 07 Nov 2006 14:03:04 +0100 |
haftmann |
made locale partial_order compatible with axclass order
|
file |
diff |
annotate
|
Tue, 07 Nov 2006 09:33:47 +0100 |
krauss |
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
|
file |
diff |
annotate
|
Tue, 04 Jul 2006 14:47:01 +0200 |
ballarin |
Method intro_locales replaced by intro_locales and unfold_locales.
|
file |
diff |
annotate
|
Tue, 20 Jun 2006 15:53:44 +0200 |
ballarin |
Restructured locales with predicates: import is now an interpretation.
|
file |
diff |
annotate
|