| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 16:32:37 +0100 |
blanchet |
merged 'List.set' with BNF-generated 'set'
|
file |
diff |
annotate
|
| Mon, 14 Oct 2013 15:01:41 +0200 |
kuncar |
declare Quotient_Examples/FSet.thy as almost obsolete
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Fri, 08 Mar 2013 09:34:38 +0100 |
traytel |
some simp rules for fset
|
file |
diff |
annotate
|
| Fri, 13 Apr 2012 14:00:26 +0200 |
wenzelm |
updated headers;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 15:15:48 +0900 |
griff |
manual merge
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 17:45:06 +0900 |
griff |
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 16:26:48 +0200 |
kuncar |
new package Lifting - initial commit
|
file |
diff |
annotate
|
| Thu, 29 Mar 2012 21:13:48 +0200 |
kuncar |
use qualified names for rsp and rep_eq theorems in quotient_def
|
file |
diff |
annotate
|
| Fri, 23 Mar 2012 14:17:29 +0100 |
kuncar |
fix Quotient_Examples
|
file |
diff |
annotate
|
| Thu, 01 Mar 2012 19:34:52 +0100 |
haftmann |
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 22:46:16 +0100 |
haftmann |
explicit is better than implicit
|
file |
diff |
annotate
|
| Thu, 09 Feb 2012 09:36:30 +0100 |
Cezary Kaliszyk |
Generalize the compositional preservation theorems
|
file |
diff |
annotate
|
| Sun, 05 Feb 2012 07:05:34 +0100 |
Cezary Kaliszyk |
Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
|
file |
diff |
annotate
|
| Fri, 03 Feb 2012 15:51:10 +0100 |
Cezary Kaliszyk |
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 10:19:49 +0100 |
haftmann |
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
|
file |
diff |
annotate
|
| Tue, 27 Dec 2011 09:45:10 +0100 |
haftmann |
be explicit about Finite_Set.fold
|
file |
diff |
annotate
|
| Mon, 26 Dec 2011 22:17:10 +0100 |
haftmann |
incorporated More_Set and More_List into the Main body -- to be consolidated later
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:05:23 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Sat, 05 Nov 2011 10:59:11 +0100 |
wenzelm |
more conventional syntax const;
|
file |
diff |
annotate
|
| 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
|
| 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
|