src/HOL/Word/Word.thy
21 months ago ago removed some non-essential rules
2018-01-16 ago standardized towards new-style formal comments: isabelle update_comments;
2018-01-12 ago prefer formal comments;
2018-01-10 ago ran isabelle update_op on all sources
2017-12-03 ago simplified session (again, see 39e29972cb96): WordExamples requires < 1s;
2017-12-02 ago more simplification rules
2017-10-24 ago generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
2017-10-08 ago elementary definition of division on natural numbers
2017-08-18 ago session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2017-04-03 ago misc tuning and modernization;
2017-03-20 ago misc tuning and modernization;
2017-03-19 ago misc tuning and modernization;
2017-03-15 ago misc tuning and modernization;
2016-12-17 ago reoriented congruence rules in non-explosive direction
2016-10-16 ago eliminated irregular aliasses
2016-10-16 ago more standardized theorem names for facts involving the div and mod identity
2016-09-26 ago syntactic type class for operation mod named after mod;
2016-09-01 ago clarified session;
2016-08-12 ago more symbols;
2016-02-23 ago more canonical names
2016-02-17 ago dropped various legacy fact bindings
2015-12-27 ago discontinued ASCII replacement syntax <->;
2015-12-10 ago not_leE -> not_le_imp_less and other tidying
2015-12-07 ago isabelle update_cartouches -c -t;
2015-11-13 ago Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-10-13 ago prod_case as canonical name for product type eliminator
2015-09-24 ago explicit indication of overloaded typedefs;
2015-09-13 ago tuned proofs -- less legacy;
2015-09-01 ago eliminated \<Colon>;
2015-07-18 ago prefer tactics with explicit context;
2015-06-12 ago uniform _ div _ as infix syntax for ring division
2015-06-01 ago separate class for division operator, with particular syntax added in more specific classes
2015-03-25 ago prefer local fixes;
2015-03-09 ago eliminated unused arith "verbose" flag -- tools that need options can use the context;
2015-02-10 ago proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
2015-02-06 ago default abstypes and default abstract equations make technical (no_code) annotation superfluous
2014-12-04 ago cleaned up mess
2014-11-10 ago proper context for assume_tac (atac remains as fall-back without context);
2014-11-02 ago modernized header;
2014-09-21 ago explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-08-28 ago renamed new SMT module from 'SMT2' to 'SMT'
2014-08-28 ago moved old setup for SMT out
2014-08-28 ago removed needless, and for (newer versions of?) Haskell problematic code equations
2014-07-27 ago do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
2014-07-05 ago prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 ago reduced name variants for assoc and commute on plus and mult
2014-06-11 ago Hypsubst preserves equality hypotheses
2014-05-16 ago added lemmas for -1
2014-03-13 ago moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
2014-03-06 ago renamed 'fun_rel' to 'rel_fun'
2014-03-02 ago repaired document;
2014-03-01 ago more precise imports;
2014-03-01 ago earlier setup of transfer, without dependency on psychodelic interpretations
2014-03-01 ago cursory polishing: tuned proofs, tuned symbols, tuned headings
2014-02-12 ago renamed 'nat_{case,rec}' to '{case,rec}_nat'
2013-12-25 ago prefer more canonical names for lemmas on min/max
2013-12-23 ago prefer "Bits" as theory name for abstract bit operations, similar to "Orderings", "Lattices", "Groups" etc.
2013-12-23 ago dropped redundant lemma
2013-12-23 ago syntactically tuned
2013-12-23 ago prefer plain bool over dedicated type for binary digits