Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
Thu, 29 Jul 2004 16:14:42 +0200 |
paulson |
removed some [iff] declarations from RealDef.thy, concerning inequalities
|
file |
diff |
annotate
|
Thu, 01 Jul 2004 12:29:53 +0200 |
paulson |
new treatment of binary numerals
|
file |
diff |
annotate
|
Thu, 24 Jun 2004 17:52:02 +0200 |
paulson |
replaced monomorphic abs definitions by abs_if
|
file |
diff |
annotate
|
Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
Sat, 01 May 2004 22:01:57 +0200 |
wenzelm |
tuned instance statements;
|
file |
diff |
annotate
|
Fri, 23 Apr 2004 11:04:07 +0200 |
paulson |
congruent2 now allows different equiv relations
|
file |
diff |
annotate
|
Thu, 22 Apr 2004 12:11:17 +0200 |
wenzelm |
constdefs: proper order;
|
file |
diff |
annotate
|
Thu, 22 Apr 2004 10:45:56 +0200 |
paulson |
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
|
file |
diff |
annotate
|
Mon, 15 Mar 2004 10:58:29 +0100 |
paulson |
heavy tidying
|
file |
diff |
annotate
|
Mon, 08 Mar 2004 11:12:06 +0100 |
paulson |
generic theorems about exponentials; general tidying up
|
file |
diff |
annotate
|
Thu, 04 Mar 2004 12:06:07 +0100 |
paulson |
new material from Avigad, and simplified treatment of division by 0
|
file |
diff |
annotate
|
Mon, 01 Mar 2004 13:51:21 +0100 |
paulson |
new Ring_and_Field hierarchy, eliminating redundant axioms
|
file |
diff |
annotate
|
Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
file |
diff |
annotate
|
Thu, 05 Feb 2004 10:45:28 +0100 |
paulson |
tidying up, especially the Complex numbers
|
file |
diff |
annotate
|
Tue, 03 Feb 2004 15:58:31 +0100 |
paulson |
further tidying of the complex numbers
|
file |
diff |
annotate
|
Tue, 03 Feb 2004 11:06:36 +0100 |
paulson |
tidying of the complex numbers
|
file |
diff |
annotate
|
Mon, 02 Feb 2004 12:23:46 +0100 |
paulson |
Conversion of HyperNat to Isar format and its declaration as a semiring
|
file |
diff |
annotate
|
Thu, 29 Jan 2004 16:51:17 +0100 |
paulson |
simplifications in the hyperreals
|
file |
diff |
annotate
|
Tue, 13 Jan 2004 10:37:52 +0100 |
paulson |
types complex and hcomplex are now instances of class ringpower:
|
file |
diff |
annotate
|
Tue, 06 Jan 2004 10:40:15 +0100 |
paulson |
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
|
file |
diff |
annotate
|
Sat, 03 Jan 2004 16:09:39 +0100 |
paulson |
Deleting more redundant theorems
|
file |
diff |
annotate
|
Thu, 01 Jan 2004 21:47:07 +0100 |
paulson |
conversion of Real/PReal to Isar script;
|
file |
diff |
annotate
|
Sat, 27 Dec 2003 21:02:14 +0100 |
paulson |
re-organized numeric lemmas
|
file |
diff |
annotate
|
Tue, 23 Dec 2003 16:53:33 +0100 |
paulson |
converting Complex/Complex.ML to Isar
|
file |
diff |
annotate
|
Tue, 23 Dec 2003 14:45:47 +0100 |
paulson |
tidying up hcomplex arithmetic
|
file |
diff |
annotate
|
Tue, 23 Dec 2003 12:54:45 +0100 |
paulson |
type hcomplex is now in class field
|
file |
diff |
annotate
|
Mon, 22 Dec 2003 18:29:20 +0100 |
paulson |
converted Complex/NSComplex to Isar script
|
file |
diff |
annotate
|
Mon, 05 May 2003 18:22:31 +0200 |
paulson |
new session Complex for the complex numbers
|
file |
diff |
annotate
|