src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
10 months ago nipkow 2018-06-14 tuned
15 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
16 months ago wenzelm 2017-12-03 misc tuning and modernization;
18 months ago haftmann 2017-10-08 replaced recdef were easy to replace
20 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2016-10-16 haftmann 2016-10-16 more standardized names
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-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-06-24 wenzelm 2015-06-24 tuned proofs -- less digits;
2015-06-23 wenzelm 2015-06-23 tuned proofs;
2015-06-22 wenzelm 2015-06-22 tuned proofs;
2015-06-20 wenzelm 2015-06-20 isabelle update_cartouches;
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-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;
2015-03-03 traytel 2015-03-03 eliminated some clones of Proof_Context.cterm_of
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
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-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
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-02-26 wenzelm 2014-02-26 tuned specifications and proofs;
2014-02-25 wenzelm 2014-02-25 tuned specifications and proofs;
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-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
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-29 wenzelm 2012-11-29 more robust syntax that survives collapse of \<^isub> and \<^sub>;
2012-11-11 haftmann 2012-11-11 modernized, simplified and compacted oracle and proof method glue code; corrected slips with poly.Pw and Orderings.less(_eq)
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-07-27 wenzelm 2012-07-27 tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-11-14 huffman 2011-11-14 Parametric_Ferrante_Rackoff.thy: restrict to class number_ring, replace '1+1' with '2' everywhere
2011-08-08 huffman 2011-08-08 moved division ring stuff from Rings.thy to Fields.thy
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy
2011-05-15 wenzelm 2011-05-15 simplified/unified method_setup/attribute_setup;
2011-04-16 wenzelm 2011-04-16 proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way; tuned;
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-02-25 nipkow 2011-02-25 Some cleaning up
2011-02-25 nipkow 2011-02-25 added simp lemma nth_Cons_pos to List
2011-02-24 krauss 2011-02-24 removed unused lemma
2011-02-23 krauss 2011-02-23 eliminated remdps in favor of List.remdups
2011-02-23 krauss 2011-02-23 recdef -> fun
2011-02-23 krauss 2011-02-23 recdef -> fun
2011-02-21 wenzelm 2011-02-21 merged, resolving spurious conflicts and giving up Reflected_Multivariate_Polynomial.thy from ab5d2d81f9fb;
2011-02-21 krauss 2011-02-21 removed duplicate declarations
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-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj