src/HOL/ex/Reflected_Presburger.thy
2007-10-20 chaieb 2007-10-20 fixed proofs
2007-08-20 nipkow 2007-08-20 Final mods for list comprehension
2007-08-20 haftmann 2007-08-20 renamed code_gen to export_code
2007-08-20 nipkow 2007-08-20 removed allpairs
2007-08-13 haftmann 2007-08-13 renamed keyword "to" to "module_name"
2007-07-26 chaieb 2007-07-26 Updated proofs; changed shadow syntax to improve (processing) time
2007-07-25 nipkow 2007-07-25 fixed broken proof
2007-07-19 haftmann 2007-07-19 uniform naming conventions for CG theories
2007-07-16 haftmann 2007-07-16 fixed SML/NJ int problem
2007-07-10 haftmann 2007-07-10 replaced code generator framework for reflected cooper
2007-06-28 haftmann 2007-06-28 new code generator framework
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-11 chaieb 2007-06-11 tuned Proof
2007-06-06 chaieb 2007-06-06 New Reflected Presburger added to HOL/ex
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-08 wenzelm 2006-11-08 moved theories Parity, GCD, Binomial to Library;
2006-06-05 krauss 2006-06-05 Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure". This simplifies some proofs.
2006-05-27 wenzelm 2006-05-27 tuned;
2006-05-12 nipkow 2006-05-12 added lemma in_measure
2006-01-04 nipkow 2006-01-04 Reversed Larry's option/iff change.
2005-12-21 paulson 2005-12-21 removed or modified some instances of [iff]
2005-09-23 webertj 2005-09-23 some typos in comments fixed
2005-09-14 wenzelm 2005-09-14 tuned headers etc.;
2005-09-14 chaieb 2005-09-14 tactic and the rest eliminated, just the theory....
2005-09-14 chaieb 2005-09-14 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy comm_ring : a reflected Method for proving equalities in a commutative ring