src/HOL/Integ/IntDef.thy
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
Tue, 06 Jan 2004 10:40:15 +0100 paulson Ring_and_Field now requires axiom add_left_imp_eq for semirings.
Wed, 03 Dec 2003 10:49:34 +0100 paulson Simplification of the development of Integers
Fri, 28 Nov 2003 12:09:37 +0100 paulson conversion of some Real theories to Isar scripts
Tue, 18 Nov 2003 11:01:52 +0100 paulson conversion of ML to Isar scripts
Thu, 08 Aug 2002 23:52:55 +0200 wenzelm tuned;
Mon, 22 Oct 2001 11:54:22 +0200 paulson Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
Mon, 08 Oct 2001 15:23:20 +0200 wenzelm sane numerals (stage 3): provide generic "1" on all number types;
Fri, 05 Oct 2001 21:52:39 +0200 wenzelm sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
Wed, 25 Jul 2001 13:13:01 +0200 paulson partial restructuring to reduce dependence on Axiom of Choice
Tue, 09 Jan 2001 15:32:27 +0100 nipkow *** empty log message ***
Fri, 05 Jan 2001 18:48:18 +0100 nipkow ^^ -> ```
Fri, 13 Oct 2000 08:28:21 +0200 nipkow *** empty log message ***
Thu, 12 Oct 2000 18:38:23 +0200 nipkow *** empty log message ***
Wed, 19 Jul 2000 12:33:36 +0200 paulson changed / to // for quotienting
Tue, 23 May 2000 18:14:57 +0200 paulson defining 0::int to be (int 0)
Fri, 27 Aug 1999 15:42:10 +0200 paulson tidied, allowing pattern-matching in defs of zadd and zmult
Thu, 29 Jul 1999 12:44:57 +0200 paulson added parentheses to cope with a possible reduction of the precedence of unary
Thu, 01 Oct 1998 18:27:17 +0200 paulson much tidying
Tue, 29 Sep 1998 15:57:42 +0200 paulson many renamings and changes. Simproc for cancelling common terms in relations
Fri, 25 Sep 1998 13:57:01 +0200 paulson Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
Wed, 23 Sep 1998 10:25:37 +0200 paulson much renaming and reorganization
Fri, 18 Sep 1998 16:04:00 +0200 paulson new files in Integ
less more (0) tip