| Wed, 12 Oct 2011 20:16:48 +0200 |
wenzelm |
tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
|
file |
diff |
annotate
|
| Fri, 26 Aug 2011 09:31:56 +0900 |
Cezary Kaliszyk |
FSet: Explicit proof without mem_def
|
file |
diff |
annotate
|
| Tue, 16 Aug 2011 07:17:15 +0900 |
Cezary Kaliszyk |
Quotient Package: make quotient_type work with separate set type
|
file |
diff |
annotate
|
| Sat, 08 Jan 2011 00:02:11 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 21:58:36 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 16:33:54 +0100 |
haftmann |
more concise case names; proved extensionality
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 17:23:14 +0100 |
wenzelm |
eliminated some hard tabulators (deprecated);
|
file |
diff |
annotate
|
| Sat, 04 Dec 2010 21:53:00 +0100 |
haftmann |
more intimate definition of fold_list / fold_once in terms of fold
|
file |
diff |
annotate
|
| Sat, 04 Dec 2010 21:26:33 +0100 |
haftmann |
canonical fold signature
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 14:46:58 +0100 |
haftmann |
conventional point-free characterization of rsp_fold
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 14:39:15 +0100 |
haftmann |
replaced memb by existing List.member
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 14:22:24 +0100 |
haftmann |
explicit type constraint;
|
file |
diff |
annotate
|
| Tue, 30 Nov 2010 17:19:11 +0100 |
haftmann |
adaptions to changes in Equiv_Relation.thy
|
file |
diff |
annotate
|
| Wed, 24 Nov 2010 19:15:00 +0100 |
haftmann |
corrected abd4e7358847 where SOMEthing went utterly wrong
|
file |
diff |
annotate
|