| 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
|
| Mon, 22 Nov 2010 17:46:51 +0100 |
haftmann |
replaced misleading Fset/fset name -- these do not stand for finite sets
|
file |
diff |
annotate
|
| Tue, 09 Nov 2010 14:02:13 +0100 |
haftmann |
more appropriate specification packages; fun_rel_def is no simp rule by default
|
file |
diff |
annotate
|
| Tue, 19 Oct 2010 15:13:35 +0100 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
| Mon, 18 Oct 2010 14:25:15 +0100 |
Christian Urban |
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
|
file |
diff |
annotate
|
| Fri, 15 Oct 2010 21:50:26 +0900 |
Cezary Kaliszyk |
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
|
file |
diff |
annotate
|