src/HOL/Word/Word_Miscellaneous.thy
21 months ago haftmann 2017-10-08 elementary definition of division on natural numbers
21 months ago haftmann 2017-10-08 avoid fact name clashes
23 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2017-04-03 wenzelm 2017-04-03 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 avoid references to lemmas designed for prover tools
2016-02-23 nipkow 2016-02-23 more canonical names
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-04-16 Lars Hupel 2015-04-16 removed trivial lemmas
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-23 haftmann 2014-10-23 downshift of theory Parity in the hierarchy
2014-10-14 haftmann 2014-10-14 legacy cleanup
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-03-01 haftmann 2014-03-01 cursory polishing: tuned proofs, tuned symbols, tuned headings
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-28 haftmann 2013-12-28 postpone dis"useful" lemmas
2013-12-28 haftmann 2013-12-28 cleanup
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