src/HOL/Quotient_Examples/FSet.thy
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