| Wed, 27 Sep 2006 07:09:19 +0200 |
huffman |
hypreal_of_nat abbreviates of_nat
|
file |
diff |
annotate
|
| Thu, 14 Sep 2006 20:31:10 +0200 |
huffman |
removed duplicate lemmas
|
file |
diff |
annotate
|
| Sat, 29 Jul 2006 13:15:12 +0200 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 23:22:29 +0200 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 23:46:22 +0200 |
huffman |
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
|
file |
diff |
annotate
|
| Fri, 09 Sep 2005 19:34:22 +0200 |
huffman |
starfun, starset, and other functions on NS types are now polymorphic;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 23:16:48 +0200 |
huffman |
replace type hypreal with real star
|
file |
diff |
annotate
|
| Wed, 27 Jul 2005 11:28:18 +0200 |
paulson |
removed the dependence on abs_mult
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| 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, 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
|
| Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
file |
diff |
annotate
|
| Tue, 10 Feb 2004 12:02:11 +0100 |
paulson |
generic of_nat and of_int functions, and generalization of iszero
|
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
|
| Wed, 28 Jan 2004 17:01:01 +0100 |
paulson |
tidying up arithmetic for the hyperreals
|
file |
diff |
annotate
|
| Mon, 12 Jan 2004 16:45:35 +0100 |
paulson |
Modified real arithmetic simplification
|
file |
diff |
annotate
|
| Thu, 25 Dec 2003 22:48:32 +0100 |
paulson |
re-organized some hyperreal and real lemmas
|
file |
diff |
annotate
|
| Mon, 22 Dec 2003 12:50:22 +0100 |
paulson |
moving HyperArith0.ML to other theories
|
file |
diff |
annotate
|
| Sat, 30 Dec 2000 22:03:47 +0100 |
paulson |
separation of HOL-Hyperreal from HOL-Real
|
file |
diff |
annotate
|