src/HOL/Library/FSet.thy
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-07-12 Lars Hupel 2015-07-12 Quickcheck setup for finite sets
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-12-05 kuncar 2014-12-05 tuned proof; forget the transfer rule for size_fset
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-06-27 blanchet 2014-06-27 merged two small theory files
2014-04-23 blanchet 2014-04-23 localize new size function generation code
2014-04-23 blanchet 2014-04-23 added 'size' of finite sets
2014-04-10 kuncar 2014-04-10 simplify and fix theories thanks to 356a5efdb278
2014-04-10 kuncar 2014-04-10 setup for Transfer and Lifting from BNF; tuned thm names
2014-04-10 kuncar 2014-04-10 abstract Domainp in relator_domain rules => more natural statement of the rule
2014-04-10 kuncar 2014-04-10 more appropriate name (Lifting.invariant -> eq_onp)
2014-04-10 kuncar 2014-04-10 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-06 blanchet 2014-03-06 renamed 'sum_rel' to 'rel_sum'
2014-03-06 blanchet 2014-03-06 renamed 'set_rel' to 'rel_set'
2014-03-06 blanchet 2014-03-06 renamed 'fset_rel' to 'rel_fset'
2014-02-25 kuncar 2014-02-25 simplify a proof due to 6c95a39348bd
2014-02-25 kuncar 2014-02-25 simplify and repair proofs due to df0fda378813
2014-02-18 kuncar 2014-02-18 simplify proofs because of the stronger reflexivity prover
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-01-24 blanchet 2014-01-24 killed 'More_BNFs' by moving its various bits where they (now) belong
2013-11-05 hoelzl 2013-11-05 use bdd_above and bdd_below for conditionally complete lattices
2013-10-01 traytel 2013-10-01 base the fset bnf on the new FSet theory
2013-09-28 wenzelm 2013-09-28 proper document markup;
2013-09-27 kuncar 2013-09-27 tuned names
2013-09-27 kuncar 2013-09-27 fold and lemmas about cardinality
2013-09-27 kuncar 2013-09-27 new theory of finite sets as a subtype