src/HOL/Enum.thy
Mon, 26 Mar 2018 16:14:16 +0200 Manuel Eberl Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Mon, 12 Mar 2018 20:52:53 +0100 Manuel Eberl Changes to complete distributive lattices due to Viorel Preoteasa
Thu, 15 Feb 2018 12:11:00 +0100 wenzelm more symbols;
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;
Mon, 09 Oct 2017 19:10:49 +0200 haftmann clarified uniqueness criterion for euclidean rings
Sun, 08 Oct 2017 22:28:22 +0200 haftmann euclidean rings need no normalization
Sun, 08 Oct 2017 22:28:21 +0200 haftmann abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
Mon, 29 May 2017 09:14:15 +0200 eberlm reorganised material on sublists
Sat, 17 Dec 2016 15:22:14 +0100 haftmann more fine-grained type class hierarchy for div and mod
Tue, 18 Oct 2016 18:48:53 +0200 haftmann suitable logical type class for abs, sgn
Mon, 26 Sep 2016 07:56:54 +0200 haftmann syntactic type class for operation mod named after mod;
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
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Fri, 12 Jun 2015 08:53:23 +0200 haftmann uniform _ div _ as infix syntax for ring division
Mon, 01 Jun 2015 18:59:21 +0200 haftmann separate class for division operator, with particular syntax added in more specific classes
Tue, 31 Mar 2015 21:54:32 +0200 haftmann given up separate type classes demanding `inverse 0 = 0`
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Mon, 20 Oct 2014 07:45:58 +0200 haftmann augmented and tuned facts on even/odd and division
Mon, 13 Oct 2014 18:45:48 +0200 wenzelm Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
Fri, 10 Oct 2014 19:55:32 +0200 haftmann specialized specification: avoid trivial instances
Tue, 16 Sep 2014 19:23:37 +0200 blanchet added 'extraction' plugins -- this might help 'HOL-Proofs'
Sun, 14 Sep 2014 22:59:30 +0200 blanchet disable datatype 'plugins' for internal types
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Wed, 03 Sep 2014 00:06:24 +0200 blanchet use 'datatype_new' in 'Main'
Sun, 31 Aug 2014 09:10:42 +0200 haftmann separated listsum material
Wed, 13 Aug 2014 17:17:51 +0200 Andreas Lochbihler add algebraic type class instances for Enum.finite* types
Fri, 08 Aug 2014 17:36:08 +0200 Andreas Lochbihler add complete_lattice instances for Enum.finite_* types such that quickcheck deals with lattice class operations
Thu, 12 Jun 2014 18:47:16 +0200 nipkow added [simp]
Mon, 20 Jan 2014 23:07:23 +0100 blanchet moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
Wed, 01 Jan 2014 01:05:48 +0100 haftmann fundamental treatment of undefined vs. universally partial replaces code_abort
Sun, 10 Nov 2013 15:05:06 +0100 haftmann qualifed popular user space names
Fri, 18 Oct 2013 10:43:21 +0200 blanchet killed more "no_atp"s
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Sun, 16 Dec 2012 18:07:29 +0100 bulwahn providing a custom code equation for vimage to overwrite the vimage definition that would be rewritten by set_comprehension_pointfree simproc in the code preprocessor to an non-terminating code equation
Mon, 22 Oct 2012 22:24:34 +0200 haftmann incorporated constant chars into instantiation proof for enum;
Sat, 20 Oct 2012 10:00:21 +0200 haftmann tailored enum specification towards simple instantiation;
Sat, 20 Oct 2012 10:00:21 +0200 haftmann refined internal structure of Enum.thy
Sat, 20 Oct 2012 09:12:16 +0200 haftmann moved quite generic material from theory Enum to more appropriate places
Mon, 25 Jun 2012 16:03:21 +0200 bulwahn some special code equations for Id with class constraint enum after adding the set comprehension simproc to the code preprocessing
Fri, 30 Mar 2012 17:25:34 +0200 wenzelm merged
Fri, 30 Mar 2012 17:22:17 +0200 wenzelm tuned proofs, less guesswork;
Fri, 30 Mar 2012 14:00:18 +0200 huffman rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
Mon, 30 Jan 2012 13:55:24 +0100 bulwahn adding code equations for max_extp and mlex
Mon, 30 Jan 2012 13:55:22 +0100 bulwahn adding code equation for rtranclp in Enum
Mon, 30 Jan 2012 13:55:21 +0100 bulwahn adding code equation for max_ext
Mon, 30 Jan 2012 13:55:20 +0100 bulwahn adding code equation for tranclp
Sat, 28 Jan 2012 12:05:26 +0100 bulwahn an executable version of accessible part (only for finite types yet)
Thu, 26 Jan 2012 12:03:35 +0100 bulwahn evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.
Wed, 25 Jan 2012 09:32:23 +0100 bulwahn adding code equation for Collect on finite types
Sat, 24 Dec 2011 15:53:08 +0100 haftmann enum type class instance for `set`; dropped misfitting code lemma for trancl
Fri, 14 Oct 2011 18:55:59 +0200 haftmann moved sublists to More_List.thy
Thu, 13 Oct 2011 23:35:15 +0200 haftmann avoid very specific code equation for card; corrected spelling
Thu, 13 Oct 2011 23:27:46 +0200 haftmann bouned transitive closure
less more (0) -60 tip