src/HOL/Quotient_Examples/FSet.thy
2013-10-14 kuncar 2013-10-14 declare Quotient_Examples/FSet.thy as almost obsolete
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-03-08 traytel 2013-03-08 some simp rules for fset
2012-04-13 wenzelm 2012-04-13 updated headers;
2012-04-04 griff 2012-04-04 manual merge
2012-04-03 griff 2012-04-03 dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit
2012-03-29 kuncar 2012-03-29 use qualified names for rsp and rep_eq theorems in quotient_def
2012-03-23 kuncar 2012-03-23 fix Quotient_Examples
2012-03-01 haftmann 2012-03-01 more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
2012-02-24 haftmann 2012-02-24 explicit is better than implicit
2012-02-09 Cezary Kaliszyk 2012-02-09 Generalize the compositional preservation theorems
2012-02-05 Cezary Kaliszyk 2012-02-05 Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
2012-02-03 Cezary Kaliszyk 2012-02-03 Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
2012-01-06 haftmann 2012-01-06 incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
2011-12-27 haftmann 2011-12-27 be explicit about Finite_Set.fold
2011-12-26 haftmann 2011-12-26 incorporated More_Set and More_List into the Main body -- to be consolidated later
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-11-05 wenzelm 2011-11-05 more conventional syntax const;
2011-10-12 wenzelm 2011-10-12 tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
2011-08-26 Cezary Kaliszyk 2011-08-26 FSet: Explicit proof without mem_def
2011-08-16 Cezary Kaliszyk 2011-08-16 Quotient Package: make quotient_type work with separate set type
2011-01-08 wenzelm 2011-01-08 tuned headers;
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-12-07 haftmann 2010-12-07 merged
2010-12-07 haftmann 2010-12-07 more concise case names; proved extensionality
2010-12-07 wenzelm 2010-12-07 eliminated some hard tabulators (deprecated);
2010-12-04 haftmann 2010-12-04 more intimate definition of fold_list / fold_once in terms of fold
2010-12-04 haftmann 2010-12-04 canonical fold signature
2010-12-03 haftmann 2010-12-03 conventional point-free characterization of rsp_fold
2010-12-03 haftmann 2010-12-03 replaced memb by existing List.member
2010-12-03 haftmann 2010-12-03 explicit type constraint; streamlined notation
2010-11-30 haftmann 2010-11-30 adaptions to changes in Equiv_Relation.thy
2010-11-24 haftmann 2010-11-24 corrected abd4e7358847 where SOMEthing went utterly wrong
2010-11-22 haftmann 2010-11-22 replaced misleading Fset/fset name -- these do not stand for finite sets
2010-11-09 haftmann 2010-11-09 more appropriate specification packages; fun_rel_def is no simp rule by default
2010-10-19 Christian Urban 2010-10-19 tuned
2010-10-18 Christian Urban 2010-10-18 reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
2010-10-15 Cezary Kaliszyk 2010-10-15 FSet: definition changes propagated from Nominal and more use of 'descending' tactic
2010-10-15 Cezary Kaliszyk 2010-10-15 FSet tuned
2010-10-15 Cezary Kaliszyk 2010-10-15 FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-06-29 Christian Urban 2010-06-29 cleaned by using descending instead of lifting
2010-06-23 Cezary Kaliszyk 2010-06-23 Replace 'list_rel' by 'list_all2'; they are equivalent.
2010-05-05 Cezary Kaliszyk 2010-05-05 fminus and some more theorems ported from Finite_Set.
2010-05-04 Cezary Kaliszyk 2010-05-04 Translating lemmas from Finite_Set to FSet.
2010-05-04 bulwahn 2010-05-04 added function ffilter and some lemmas from Finite_Set to the FSet theory
2010-04-29 Cezary Kaliszyk 2010-04-29 Tuning the quotient examples
2010-04-28 Cezary Kaliszyk 2010-04-28 Tuned FSet
2010-04-26 Cezary Kaliszyk 2010-04-26 add bounded_lattice_bot and bounded_lattice_top type classes
2010-04-23 Cezary Kaliszyk 2010-04-23 Finite set theory