src/HOL/Integ/IntDef.thy
Sun, 23 Jul 2006 07:21:22 +0200 haftmann fixed bug for serialization for uminus on ints
Fri, 21 Jul 2006 14:48:35 +0200 haftmann simplification for code generation for Integers
Wed, 12 Jul 2006 17:00:22 +0200 haftmann adaptions in codegen
Wed, 14 Jun 2006 12:12:37 +0200 haftmann slight refinements for code generator
Tue, 16 May 2006 21:33:01 +0200 wenzelm tuned concrete syntax -- abbreviation/const_syntax;
Tue, 09 May 2006 10:10:28 +0200 haftmann added codegen preprocessors for numerals
Tue, 02 May 2006 20:42:30 +0200 wenzelm replaced syntax/translations by abbreviation;
Thu, 06 Apr 2006 16:12:57 +0200 haftmann added explicit serialization for int equality
Fri, 17 Mar 2006 09:34:23 +0100 haftmann renamed op < <= to Orderings.less(_eq)
Fri, 10 Mar 2006 15:33:48 +0100 haftmann renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
Sat, 25 Feb 2006 15:19:47 +0100 haftmann improved codegen bootstrap
Wed, 15 Feb 2006 19:01:09 +0100 nipkow got rid of superfluous linorder_neqE-instance for int.
Fri, 03 Feb 2006 08:48:16 +0100 haftmann fix in codegen
Mon, 23 Jan 2006 14:07:52 +0100 haftmann removed problematic keyword 'atom'
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Wed, 18 Jan 2006 11:55:50 +0100 haftmann substantial improvement in serialization handling
Tue, 17 Jan 2006 16:36:57 +0100 haftmann substantial improvements in code generator
Thu, 29 Dec 2005 15:31:10 +0100 haftmann adaptions to changes in code generator
Fri, 02 Dec 2005 16:05:12 +0100 haftmann adjusted to improved code generator interface
Tue, 22 Nov 2005 12:59:25 +0100 haftmann added codegenerator
Tue, 08 Nov 2005 09:13:22 +0100 haftmann (fix for accidental commit)
Tue, 08 Nov 2005 09:12:02 +0100 haftmann (codegen)
Tue, 27 Sep 2005 12:14:39 +0200 berghofe Inserted clause for nat in number_of_codegen again ("code unfold" turned
Wed, 21 Sep 2005 12:02:56 +0200 berghofe Simplified code generator for numerals.
Sat, 17 Sep 2005 18:11:24 +0200 wenzelm added quickcheck_params (from Main.thy);
Tue, 16 Aug 2005 18:53:11 +0200 paulson more simprules now have names
Tue, 12 Jul 2005 11:51:31 +0200 berghofe Auxiliary functions to be used in generated code are now defined using "attach".
Thu, 07 Jul 2005 12:39:17 +0200 nipkow linear arithmetic now takes "&" in assumptions apart.
Fri, 01 Jul 2005 14:08:53 +0200 berghofe Moved code generator setup from NatBin to IntDef.
Thu, 16 Jun 2005 19:51:04 +0200 paulson a few new integer lemmas
Wed, 04 May 2005 08:36:10 +0200 nipkow Fixing a problem with lin.arith.
Wed, 02 Mar 2005 10:02:21 +0100 paulson new lemmas int_diff_cases
Tue, 01 Mar 2005 18:48:52 +0100 nipkow integrated Jeremy's FiniteLib
Mon, 21 Feb 2005 15:57:45 +0100 nipkow removed superfluous setsum_constant
Mon, 21 Feb 2005 15:04:10 +0100 nipkow comprehensive cleanup, replacing sumr by setsum
Tue, 01 Feb 2005 18:01:57 +0100 paulson the new subst tactic, by Lucas Dixon
Wed, 15 Dec 2004 17:32:40 +0100 paulson removal of archaic Abs/Rep proofs
Tue, 14 Dec 2004 10:45:16 +0100 paulson new and stronger lemmas and improved simplification for finite sets
Fri, 19 Nov 2004 17:31:49 +0100 paulson moved and renamed Integ/Equiv.thy
Tue, 19 Oct 2004 18:18:45 +0200 paulson converted some induct_tac to induct
Wed, 01 Sep 2004 15:04:01 +0200 paulson new "respects" syntax for quotienting
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Thu, 15 Jul 2004 15:32:32 +0200 paulson redefining sumr to be a translation to setsum
Thu, 01 Jul 2004 12:29:53 +0200 paulson new treatment of binary numerals
Thu, 24 Jun 2004 17:52:02 +0200 paulson replaced monomorphic abs definitions by abs_if
Wed, 12 May 2004 10:00:56 +0200 nipkow fixed latex problems
Tue, 11 May 2004 20:11:08 +0200 obua changes made due to new Ring_and_Field theory
Sat, 01 May 2004 22:01:57 +0200 wenzelm tuned instance statements;
Fri, 23 Apr 2004 11:04:07 +0200 paulson congruent2 now allows different equiv relations
Thu, 08 Apr 2004 15:14:33 +0200 paulson tidied
Tue, 30 Mar 2004 11:18:12 +0200 paulson tidied
Thu, 25 Mar 2004 10:32:21 +0100 paulson new material from Avigad
Wed, 24 Mar 2004 10:50:29 +0100 paulson streamlined treatment of quotients for the integers
Thu, 04 Mar 2004 12:06:07 +0100 paulson new material from Avigad, and simplified treatment of division by 0
Mon, 01 Mar 2004 13:51:21 +0100 paulson new Ring_and_Field hierarchy, eliminating redundant axioms
Thu, 19 Feb 2004 15:57:34 +0100 ballarin Efficient, graph-based reasoner for linear and partial orders.
Sun, 15 Feb 2004 10:46:37 +0100 paulson Polymorphic treatment of binary arithmetic using axclasses
Tue, 10 Feb 2004 12:02:11 +0100 paulson generic of_nat and of_int functions, and generalization of iszero
Fri, 09 Jan 2004 10:46:18 +0100 paulson Defining the type class "ringpower" and deleting superseded theorems for
less more (0) -60 tip