2016-04-08 wenzelm 2016-04-08 eliminated unused simproc identifier;
2016-02-23 nipkow 2016-02-23 more canonical names
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-03-06 wenzelm 2015-03-06 clarified context;
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-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-02-14 blanchet 2014-02-14 merged '' and ''
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-12-23 haftmann 2013-12-23 prefer plain bool over dedicated type for binary digits
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-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-10 wenzelm 2013-04-10 added ML antiquotation @{theory_context};
2013-01-15 wenzelm 2013-01-15 avoid handling arbitrary exceptions, notably physical interrupts that would make the program erratic;
2012-11-17 wenzelm 2012-11-17 tuned signature;
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-04-17 Thomas Sewell 2012-04-17 New tactic "word_bitwise" expands word equalities/inequalities into logic.
2010-06-30 haftmann 2010-06-30 use existing bit type from theory Bit
2010-01-20 bulwahn 2010-01-20 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
2009-04-27 haftmann 2009-04-27 explicit is better than implicit
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-01-26 haftmann 2009-01-26 stripped Id
2008-12-16 ballarin 2008-12-16 More porting to new locales.
2008-05-07 berghofe 2008-05-07 Deleted subset_antisym in a few proofs, because it is accidentally applied to predicates as well.
2008-04-04 haftmann 2008-04-04 renamed app2 to map2
2008-03-15 wenzelm 2008-03-15 avoid unclear fact references;
2007-11-08 wenzelm 2007-11-08 eliminated illegal schematic variables in where/of;
2007-08-28 huffman 2007-08-28 revert to Word library version from 2007/08/20
2007-08-22 huffman 2007-08-22 removed Word/Size.thy; replaced len_of TYPE('a) with CARD('a); replaced axclass len with class finite; replaced axclass len0 with class type
2007-08-22 huffman 2007-08-22 move bool list operations from WordBitwise to WordBoolList
2007-08-22 huffman 2007-08-22 move bool list stuff from WordDefinition and WordArith to new WordBoolList theory
2007-08-20 huffman 2007-08-20 remove redundant lemma int_number_of
2007-08-20 huffman 2007-08-20 AC rules for bitwise logical operators no longer declared simp
2007-08-20 huffman 2007-08-20 use overloaded bitwise operators at type int
2007-08-20 huffman 2007-08-20 headers for document generation
2007-08-20 kleing 2007-08-20 * HOL-Word: New extensive library and type for generic, fixed size machine words, with arithemtic, bit-wise, shifting and rotating operations, reflection into int, nat, and bool lists, automation for linear arithmetic (by automatic reflection into nat or int), including lemmas on overflow and monotonicity. Instantiated to all appropriate arithmetic type classes, supporting automatic simplification of numerals on all operations. Jointly developed by NICTA, Galois, and PSU. * still to do: README.html/document + moving some of the generic lemmas to appropriate place in distribution