src/HOL/Proofs/Extraction/Euclid.thy
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Wed, 19 Oct 2011 08:37:15 +0200 bulwahn removing invocations of the evaluation method based on the old code generator
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Mon, 06 Sep 2010 14:18:16 +0200 wenzelm 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);
less more (0) tip