src/HOL/Library/FSet.thy
5 months ago paulson 2019-01-22 renamings and new material
5 months ago paulson 2019-01-21 new material about summations and powers, along with some tweaks
6 months ago nipkow 2019-01-14 uniform naming
6 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
8 months ago nipkow 2018-10-21 uniform naming of strong congruence rules
13 months ago Lars Hupel 2018-06-18 material on finite sets and maps
16 months ago Manuel Eberl 2018-03-12 Changes to complete distributive lattices due to Viorel Preoteasa
16 months ago ballarin 2018-03-04 Drop rewrites after defines in interpretations.
18 months ago wenzelm 2018-01-12 prefer formal comments;
18 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
19 months ago wenzelm 2017-11-26 more symbols;
24 months ago Lars Hupel 2017-07-20 improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
2017-07-11 Lars Hupel 2017-07-11 card_0_eq ~> fcard_0_eq
2017-07-11 Lars Hupel 2017-07-11 material from $AFP/Formula_Derivatives/FSet_More
2017-07-10 Lars Hupel 2017-07-10 finite sets are countable
2017-07-10 Lars Hupel 2017-07-10 lift sum to finite sets
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-08-10 wenzelm 2016-08-10 tuned proofs;
2016-08-06 Lars Hupel 2016-08-06 some additions to FSet
2016-06-22 wenzelm 2016-06-22 bundle lifting_syntax;
2016-06-17 hoelzl 2016-06-17 move Conditional_Complete_Lattices to Main
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-02-16 traytel 2016-02-16 make predicator a first-class bnf citizen
2016-01-07 paulson 2016-01-07 revisions to limits and derivatives, plus new lemmas
2016-01-06 blanchet 2016-01-06 nicer 'Spec_Rules' for size function
2015-12-28 wenzelm 2015-12-28 prefer symbols for "Union", "Inter";
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
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