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