src/HOL/Decision_Procs/MIR.thy
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-06-20 wenzelm 2015-06-20 isabelle update_cartouches;
2015-06-01 wenzelm 2015-06-01 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-11-05 wenzelm 2014-11-05 more symbols;
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 ported Decision_Procs to new datatypes
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-08-07 blanchet 2014-08-07 no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-11 Thomas Sewell 2014-06-11 Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.
2014-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-04-09 hoelzl 2014-04-09 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
2014-04-04 paulson 2014-04-04 divide_minus_left divide_minus_right are in field_simps but are not default simprules
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2014-02-19 blanchet 2014-02-19 merged 'List.set' with BNF-generated 'set'
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-08-23 wenzelm 2013-08-23 tuned signature;
2013-03-07 wenzelm 2013-03-07 tuned proofs -- more structure, less warnings;
2013-02-25 wenzelm 2013-02-25 prefer stateless 'ML_val' for tests;
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2012-11-28 wenzelm 2012-11-28 eliminated slightly odd identifiers;
2012-11-27 wenzelm 2012-11-27 eliminated some improper identifiers;
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-09-03 wenzelm 2012-09-03 some parallel ML;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-12 wenzelm 2012-04-12 more standard method setup;
2012-03-27 huffman 2012-03-27 remove redundant lemmas
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-02-25 bulwahn 2012-02-25 removing unnecessary assumptions in RealDef; simplifying proofs in Float, MIR, and Ferrack
2012-01-06 haftmann 2012-01-06 prefer concat over foldl append []
2011-12-02 wenzelm 2011-12-02 more antiquotations;
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy
2011-03-03 wenzelm 2011-03-03 tuned proofs -- eliminated prems;
2011-03-03 wenzelm 2011-03-03 removed spurious 'unused_thms' (cf. 1a65b780bd56);
2011-02-25 nipkow 2011-02-25 Some cleaning up
2011-02-24 krauss 2011-02-24 recdef -> fun(ction)
2011-02-24 krauss 2011-02-24 eliminated clones of List.upto
2011-02-21 wenzelm 2011-02-21 tuned proofs -- eliminated prems;
2011-01-07 bulwahn 2011-01-07 adopting proofs due to new list comprehension to set comprehension simproc
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-07-19 haftmann 2010-07-19 diff_minus subsumes diff_def
2010-05-12 haftmann 2010-05-12 tuned test problems
2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2010-04-29 haftmann 2010-04-29 code_reflect: specify module name directly after keyword
2010-04-28 haftmann 2010-04-28 use code_reflect
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-11-12 hoelzl 2009-11-12 New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key