src/HOL/ex/Reflected_Presburger.thy
Sun, 02 Dec 2007 20:38:42 +0100 chaieb Eliminated unused theorems minusinf_ex and minusinf_bex
Tue, 23 Oct 2007 23:27:23 +0200 nipkow went back to >0
Sun, 21 Oct 2007 14:53:44 +0200 nipkow Eliminated most of the neq0_conv occurrences. As a result, many
Sat, 20 Oct 2007 12:09:33 +0200 chaieb fixed proofs
Mon, 20 Aug 2007 18:10:13 +0200 nipkow Final mods for list comprehension
Mon, 20 Aug 2007 18:07:49 +0200 haftmann renamed code_gen to export_code
Mon, 20 Aug 2007 11:18:18 +0200 nipkow removed allpairs
Mon, 13 Aug 2007 21:22:37 +0200 haftmann renamed keyword "to" to "module_name"
Thu, 26 Jul 2007 21:49:53 +0200 chaieb Updated proofs; changed shadow syntax to improve (processing) time
Wed, 25 Jul 2007 18:10:49 +0200 nipkow fixed broken proof
Thu, 19 Jul 2007 21:47:39 +0200 haftmann uniform naming conventions for CG theories
Mon, 16 Jul 2007 09:29:01 +0200 haftmann fixed SML/NJ int problem
Tue, 10 Jul 2007 09:23:15 +0200 haftmann replaced code generator framework for reflected cooper
Thu, 28 Jun 2007 19:09:38 +0200 haftmann new code generator framework
Sat, 23 Jun 2007 19:33:22 +0200 nipkow tuned and renamed group_eq_simps and ring_eq_simps
Mon, 11 Jun 2007 11:06:04 +0200 chaieb tuned Proof
Wed, 06 Jun 2007 16:12:08 +0200 chaieb New Reflected Presburger added to HOL/ex
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Wed, 08 Nov 2006 23:11:13 +0100 wenzelm moved theories Parity, GCD, Binomial to Library;
Mon, 05 Jun 2006 14:22:58 +0200 krauss Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
Sat, 27 May 2006 17:42:02 +0200 wenzelm tuned;
Fri, 12 May 2006 11:19:41 +0200 nipkow added lemma in_measure
Wed, 04 Jan 2006 19:22:53 +0100 nipkow Reversed Larry's option/iff change.
Wed, 21 Dec 2005 12:02:57 +0100 paulson removed or modified some instances of [iff]
Fri, 23 Sep 2005 21:02:13 +0200 webertj some typos in comments fixed
Wed, 14 Sep 2005 22:08:08 +0200 wenzelm tuned headers etc.;
Wed, 14 Sep 2005 21:44:27 +0200 chaieb tactic and the rest eliminated, just the theory....
Wed, 14 Sep 2005 17:25:52 +0200 chaieb The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
less more (0) tip