src/HOL/Library/FSet.thy
Mon, 12 Mar 2018 20:52:53 +0100 Manuel Eberl Changes to complete distributive lattices due to Viorel Preoteasa
Sun, 04 Mar 2018 12:22:48 +0100 ballarin Drop rewrites after defines in interpretations.
Fri, 12 Jan 2018 15:27:46 +0100 wenzelm prefer formal comments;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Thu, 20 Jul 2017 17:13:17 +0200 Lars Hupel improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Tue, 11 Jul 2017 09:31:36 +0200 Lars Hupel card_0_eq ~> fcard_0_eq
Tue, 11 Jul 2017 09:22:14 +0200 Lars Hupel material from $AFP/Formula_Derivatives/FSet_More
Mon, 10 Jul 2017 18:53:38 +0200 Lars Hupel finite sets are countable
Mon, 10 Jul 2017 16:38:42 +0200 Lars Hupel lift sum to finite sets
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Wed, 10 Aug 2016 14:50:59 +0200 wenzelm tuned proofs;
Sat, 06 Aug 2016 13:36:49 +0200 Lars Hupel some additions to FSet
Wed, 22 Jun 2016 10:09:20 +0200 wenzelm bundle lifting_syntax;
Fri, 17 Jun 2016 09:44:16 +0200 hoelzl move Conditional_Complete_Lattices to Main
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Tue, 16 Feb 2016 22:28:19 +0100 traytel make predicator a first-class bnf citizen
Thu, 07 Jan 2016 17:40:55 +0000 paulson revisions to limits and derivatives, plus new lemmas
Wed, 06 Jan 2016 13:04:31 +0100 blanchet nicer 'Spec_Rules' for size function
Mon, 28 Dec 2015 17:43:30 +0100 wenzelm prefer symbols for "Union", "Inter";
Thu, 05 Nov 2015 10:39:49 +0100 wenzelm isabelle update_cartouches -c -t;
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Sun, 12 Jul 2015 13:04:42 +0200 Lars Hupel Quickcheck setup for finite sets
Mon, 06 Jul 2015 22:57:34 +0200 wenzelm tuned proofs;
Wed, 17 Jun 2015 11:03:05 +0200 wenzelm isabelle update_cartouches;
Fri, 05 Dec 2014 14:14:36 +0100 kuncar tuned proof; forget the transfer rule for size_fset
Sun, 02 Nov 2014 17:20:45 +0100 wenzelm modernized header;
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Fri, 27 Jun 2014 10:11:44 +0200 blanchet merged two small theory files
Wed, 23 Apr 2014 10:23:27 +0200 blanchet localize new size function generation code
Wed, 23 Apr 2014 10:23:27 +0200 blanchet added 'size' of finite sets
Thu, 10 Apr 2014 17:48:32 +0200 kuncar simplify and fix theories thanks to 356a5efdb278
Thu, 10 Apr 2014 17:48:18 +0200 kuncar setup for Transfer and Lifting from BNF; tuned thm names
Thu, 10 Apr 2014 17:48:15 +0200 kuncar abstract Domainp in relator_domain rules => more natural statement of the rule
Thu, 10 Apr 2014 17:48:15 +0200 kuncar more appropriate name (Lifting.invariant -> eq_onp)
Thu, 10 Apr 2014 17:48:14 +0200 kuncar left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
Sun, 16 Mar 2014 18:09:04 +0100 haftmann normalising simp rules for compound operators
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Thu, 06 Mar 2014 15:25:21 +0100 blanchet renamed 'sum_rel' to 'rel_sum'
Thu, 06 Mar 2014 14:57:14 +0100 blanchet renamed 'set_rel' to 'rel_set'
Thu, 06 Mar 2014 13:36:49 +0100 blanchet renamed 'fset_rel' to 'rel_fset'
Tue, 25 Feb 2014 19:07:42 +0100 kuncar simplify a proof due to 6c95a39348bd
Tue, 25 Feb 2014 15:02:20 +0100 kuncar simplify and repair proofs due to df0fda378813
Tue, 18 Feb 2014 23:03:50 +0100 kuncar simplify proofs because of the stronger reflexivity prover
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Fri, 24 Jan 2014 11:51:45 +0100 blanchet killed 'More_BNFs' by moving its various bits where they (now) belong
Tue, 05 Nov 2013 09:44:58 +0100 hoelzl use bdd_above and bdd_below for conditionally complete lattices
Tue, 01 Oct 2013 17:06:35 +0200 traytel base the fset bnf on the new FSet theory
Sat, 28 Sep 2013 14:41:46 +0200 wenzelm proper document markup;
Fri, 27 Sep 2013 21:54:55 +0200 kuncar tuned names
Fri, 27 Sep 2013 21:54:55 +0200 kuncar fold and lemmas about cardinality
Fri, 27 Sep 2013 14:43:26 +0200 kuncar new theory of finite sets as a subtype
less more (0) tip