| 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
|
| 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
|
| Fri, 15 Oct 2010 21:47:45 +0900 |
Cezary Kaliszyk |
FSet tuned
|
file |
diff |
annotate
|
| Fri, 15 Oct 2010 21:46:45 +0900 |
Cezary Kaliszyk |
FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 17:03:59 +0100 |
Christian Urban |
cleaned by using descending instead of lifting
|
file |
diff |
annotate
|
| Wed, 23 Jun 2010 08:42:41 +0200 |
Cezary Kaliszyk |
Replace 'list_rel' by 'list_all2'; they are equivalent.
|
file |
diff |
annotate
|
| Wed, 05 May 2010 15:30:01 +0200 |
Cezary Kaliszyk |
fminus and some more theorems ported from Finite_Set.
|
file |
diff |
annotate
|
| Tue, 04 May 2010 16:25:16 +0200 |
Cezary Kaliszyk |
Translating lemmas from Finite_Set to FSet.
|
file |
diff |
annotate
|
| Tue, 04 May 2010 11:00:16 +0200 |
bulwahn |
added function ffilter and some lemmas from Finite_Set to the FSet theory
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 09:06:35 +0200 |
Cezary Kaliszyk |
Tuning the quotient examples
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 13:29:40 +0200 |
Cezary Kaliszyk |
Tuned FSet
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 15:14:14 +0200 |
Cezary Kaliszyk |
add bounded_lattice_bot and bounded_lattice_top type classes
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 10:00:53 +0200 |
Cezary Kaliszyk |
Finite set theory
|
file |
diff |
annotate
|