src/HOL/Decision_Procs/Cooper.thy
7 months ago wenzelm 2018-11-08 proper ML expressions, without trailing semicolons;
7 months ago wenzelm 2018-10-31 tuned;
8 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.
17 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
18 months ago wenzelm 2017-12-03 misc tuning and modernization;
20 months ago haftmann 2017-10-08 replaced recdef were easy to replace
22 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2017-02-11 haftmann 2017-02-11 more fun without recdef
2016-10-16 haftmann 2016-10-16 eliminated irregular aliasses
2016-02-17 haftmann 2016-02-17 consolidated name
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-07-09 wenzelm 2015-07-09 tuned proofs;
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;
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-03-08 wenzelm 2014-03-08 tuned proofs;
2014-03-07 wenzelm 2014-03-07 tuned proofs;
2014-03-06 wenzelm 2014-03-06 tuned proofs;
2014-03-05 wenzelm 2014-03-05 tuned proofs;
2014-03-05 wenzelm 2014-03-05 tuned proofs;
2014-03-03 wenzelm 2014-03-03 tuned proofs;
2014-03-02 wenzelm 2014-03-02 tuned proofs;
2014-02-28 wenzelm 2014-02-28 tuned whitespace; more symbols;
2014-02-23 haftmann 2014-02-23 regenerated
2014-02-19 blanchet 2014-02-19 merged 'List.set' with BNF-generated 'set'
2014-02-12 blanchet 2014-02-12 compile
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
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-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
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-12-02 wenzelm 2012-12-02 misc tuning;
2012-11-28 wenzelm 2012-11-28 eliminated slightly odd identifiers;
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
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)
2011-12-02 wenzelm 2011-12-02 more antiquotations;
2011-09-14 haftmann 2011-09-14 updated comment
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-07 huffman 2011-09-07 avoid using legacy theorem names
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-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-02-24 krauss 2011-02-24 recdef -> fun(ction); tuned
2011-02-24 krauss 2011-02-24 eliminated clones of List.upto
2011-02-21 wenzelm 2011-02-21 tuned proofs -- eliminated prems;
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-09-08 haftmann 2010-09-08 modernized primrec
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj