2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-09-24 wenzelm 2015-09-24 explicit indication of overloaded typedefs;
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 prefer tactics with explicit context;
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-25 wenzelm 2015-03-25 prefer local fixes;
2015-03-09 wenzelm 2015-03-09 eliminated unused arith "verbose" flag -- tools that need options can use the context;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2015-02-06 haftmann 2015-02-06 default abstypes and default abstract equations make technical (no_code) annotation superfluous
2014-12-04 haftmann 2014-12-04 cleaned up mess
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2014-08-28 blanchet 2014-08-28 moved old setup for SMT out
2014-08-28 blanchet 2014-08-28 removed needless, and for (newer versions of?) Haskell problematic code equations
2014-07-27 blanchet 2014-07-27 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
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-05-16 noschinl 2014-05-16 added lemmas for -1
2014-03-13 blanchet 2014-03-13 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-02 wenzelm 2014-03-02 repaired document;
2014-03-01 haftmann 2014-03-01 more precise imports; avoid duplicated simp rules in fact collections; dropped redundancy
2014-03-01 haftmann 2014-03-01 earlier setup of transfer, without dependency on psychodelic interpretations
2014-03-01 haftmann 2014-03-01 cursory polishing: tuned proofs, tuned symbols, tuned headings
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-12-23 haftmann 2013-12-23 prefer "Bits" as theory name for abstract bit operations, similar to "Orderings", "Lattices", "Groups" etc.
2013-12-23 haftmann 2013-12-23 dropped redundant lemma
2013-12-23 haftmann 2013-12-23 syntactically tuned
2013-12-23 haftmann 2013-12-23 prefer plain bool over dedicated type for binary digits
2013-12-14 wenzelm 2013-12-14 more antiquotations;
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-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-10-31 haftmann 2013-10-31 generalized of_bool conversion
2013-10-31 haftmann 2013-10-31 separated bit operations on type bit from generic syntactic bit operations
2013-10-31 haftmann 2013-10-31 more lemmas on division
2013-08-18 wenzelm 2013-08-18 tuned;
2013-08-18 haftmann 2013-08-18 some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-03-08 kuncar 2013-03-08 patch Isabelle ditribution to conform to changes regarding the parametricity
2013-02-26 wenzelm 2013-02-26 tuned;
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-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-07-05 wenzelm 2012-07-05 explicit is better than implicit;
2012-05-18 kuncar 2012-05-18 don't generate code in Word because it breaks the current code setup
2012-04-19 huffman 2012-04-19 add code lemmas for word operations
2012-04-17 Thomas Sewell 2012-04-17 New tactic "word_bitwise" expands word equalities/inequalities into logic.
2012-04-18 kuncar 2012-04-18 setup_lifting: no_code switch and supoport for quotient theorems
2012-04-17 kuncar 2012-04-17 tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
2012-04-06 huffman 2012-04-06 remove now-unnecessary type annotations from lift_definition commands
2012-04-05 huffman 2012-04-05 use standard quotient lemmas to generate transfer rules
2012-04-05 huffman 2012-04-05 set up and use lift_definition for word operations
2012-04-05 huffman 2012-04-05 configure transfer method for 'a word -> int