src/HOL/Word/Word.thy
2017-04-03 wenzelm 2017-04-03 misc tuning and modernization;
2017-03-20 wenzelm 2017-03-20 misc tuning and modernization;
2017-03-19 wenzelm 2017-03-19 misc tuning and modernization;
2017-03-15 wenzelm 2017-03-15 misc tuning and modernization;
2016-12-17 haftmann 2016-12-17 reoriented congruence rules in non-explosive direction
2016-10-16 haftmann 2016-10-16 eliminated irregular aliasses
2016-10-16 haftmann 2016-10-16 more standardized theorem names for facts involving the div and mod identity
2016-09-26 haftmann 2016-09-26 syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div
2016-09-01 wenzelm 2016-09-01 clarified session; misc tuning and modernization;
2016-08-12 wenzelm 2016-08-12 more symbols;
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2015-12-27 wenzelm 2015-12-27 discontinued ASCII replacement syntax <->;
2015-12-10 paulson 2015-12-10 not_leE -> not_le_imp_less and other tidying
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
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;