3 months ago wenzelm 2019-02-28 tuned proofs -- eliminated odd case_tac;
4 months ago haftmann 2019-01-31 proper congruence rule for image operator
5 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
7 months ago haftmann 2018-11-10 clarified status of legacy input abbreviations
9 months ago nipkow 2018-09-24 Prefix form of infix with * on either side no longer needs special treatment because (* and *) are no longer comment brackets in terms.
15 months ago Manuel Eberl 2018-03-26 Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
15 months ago Manuel Eberl 2018-03-12 Changes to complete distributive lattices due to Viorel Preoteasa
16 months ago wenzelm 2018-02-15 more symbols;
17 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
19 months ago wenzelm 2017-11-26 more symbols;
20 months ago haftmann 2017-10-09 clarified uniqueness criterion for euclidean rings
20 months ago haftmann 2017-10-08 euclidean rings need no normalization
20 months ago haftmann 2017-10-08 abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
2017-05-29 eberlm 2017-05-29 reorganised material on sublists
2016-12-17 haftmann 2016-12-17 more fine-grained type class hierarchy for div and mod
2016-10-18 haftmann 2016-10-18 suitable logical type class for abs, sgn
2016-09-26 haftmann 2016-09-26 syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div
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
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-12 haftmann 2015-06-12 uniform _ div _ as infix syntax for ring division
2015-06-01 haftmann 2015-06-01 separate class for division operator, with particular syntax added in more specific classes
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-20 haftmann 2014-10-20 augmented and tuned facts on even/odd and division
2014-10-13 wenzelm 2014-10-13 Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
2014-10-10 haftmann 2014-10-10 specialized specification: avoid trivial instances
2014-09-16 blanchet 2014-09-16 added 'extraction' plugins -- this might help 'HOL-Proofs'
2014-09-14 blanchet 2014-09-14 disable datatype 'plugins' for internal types
2014-09-11 blanchet 2014-09-11 updated news
2014-09-03 blanchet 2014-09-03 use 'datatype_new' in 'Main'
2014-08-31 haftmann 2014-08-31 separated listsum material
2014-08-13 Andreas Lochbihler 2014-08-13 add algebraic type class instances for Enum.finite* types
2014-08-08 Andreas Lochbihler 2014-08-08 add complete_lattice instances for Enum.finite_* types such that quickcheck deals with lattice class operations
2014-06-12 nipkow 2014-06-12 added [simp]
2014-01-20 blanchet 2014-01-20 moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
2014-01-01 haftmann 2014-01-01 fundamental treatment of undefined vs. universally partial replaces code_abort
2013-11-10 haftmann 2013-11-10 qualifed popular user space names
2013-10-18 blanchet 2013-10-18 killed more "no_atp"s
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2012-12-16 bulwahn 2012-12-16 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
2012-10-22 haftmann 2012-10-22 incorporated constant chars into instantiation proof for enum; tuned proofs for properties on enum of chars; swapped theory dependency of Enum.thy and String.thy
2012-10-20 haftmann 2012-10-20 tailored enum specification towards simple instantiation; tuned enum instantiations
2012-10-20 haftmann 2012-10-20 refined internal structure of Enum.thy
2012-10-20 haftmann 2012-10-20 moved quite generic material from theory Enum to more appropriate places
2012-06-25 bulwahn 2012-06-25 some special code equations for Id with class constraint enum after adding the set comprehension simproc to the code preprocessing
2012-03-30 wenzelm 2012-03-30 merged
2012-03-30 wenzelm 2012-03-30 tuned proofs, less guesswork;
2012-03-30 huffman 2012-03-30 rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
2012-01-30 bulwahn 2012-01-30 adding code equations for max_extp and mlex
2012-01-30 bulwahn 2012-01-30 adding code equation for rtranclp in Enum
2012-01-30 bulwahn 2012-01-30 adding code equation for max_ext
2012-01-30 bulwahn 2012-01-30 adding code equation for tranclp
2012-01-28 bulwahn 2012-01-28 an executable version of accessible part (only for finite types yet)
2012-01-26 bulwahn 2012-01-26 evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.