src/HOL/Decision_Procs/MIR.thy
7 months ago wenzelm 2018-11-08 proper ML expressions, without trailing semicolons;
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.
13 months ago haftmann 2018-05-24 treat gcd_eq_1_imp_coprime analogously to mod_0_imp_dvd
16 months ago wenzelm 2018-02-15 more symbols;
17 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
18 months ago haftmann 2017-12-02 more simplification rules
20 months ago haftmann 2017-10-08 replaced recdef were easy to replace
22 months ago nipkow 2017-08-26 reorganized and added log-related lemmas
22 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2017-06-20 haftmann 2017-06-20 replaced recdef by fun
2017-06-20 haftmann 2017-06-20 spelling
2016-10-16 haftmann 2016-10-16 eliminated irregular aliasses
2016-10-16 haftmann 2016-10-16 more standardized names
2016-08-05 nipkow 2016-08-05 fixed floor proof
2016-02-17 haftmann 2016-02-17 consolidated name
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-12-27 wenzelm 2015-12-27 prefer symbols for "floor", "ceiling";
2015-12-01 paulson 2015-12-01 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-11-17 paulson 2015-11-17 Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
2015-11-13 paulson 2015-11-13 MIR decision procedure again working
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-10 paulson 2015-11-10 Merge
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
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-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 []