src/HOL/Proofs/Extraction/Euclid.thy
2016-08-08 eberlm 2016-08-08 is_prime -> prime
2016-07-22 eberlm 2016-07-22 Removed redundant material related to primes
2016-07-21 eberlm 2016-07-21 Overhaul of prime/multiplicity/prime_factors
2016-07-01 wenzelm 2016-07-01 misc tuning and modernization;
2015-12-30 wenzelm 2015-12-30 isabelle update_cartouches -c -t;
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-12-01 paulson 2015-12-01 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-06-19 nipkow 2015-06-19 renamed multiset_of -> mset
2015-03-16 paulson 2015-03-16 The factorial function, "fact", now has type "nat => 'a"
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-07 wenzelm 2014-10-07 more antiquotations;
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
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
2011-10-19 bulwahn 2011-10-19 removing invocations of the evaluation method based on the old code generator
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-09-06 wenzelm 2010-09-06 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);