| 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
|
| Wed, 07 Sep 2005 02:13:24 +0200 |
huffman |
added theorem hypreal_inverse2
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 23:16:48 +0200 |
huffman |
replace type hypreal with real star
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 19:22:31 +0200 |
huffman |
reimplement Filter.thy with locales
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Mon, 21 Feb 2005 15:04:10 +0100 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
file |
diff |
annotate
|
| Wed, 15 Dec 2004 17:32:40 +0100 |
paulson |
removal of archaic Abs/Rep proofs
|
file |
diff |
annotate
|
| Thu, 07 Oct 2004 15:42:30 +0200 |
paulson |
simplification tweaks for better arithmetic reasoning
|
file |
diff |
annotate
|
| Tue, 05 Oct 2004 15:30:50 +0200 |
paulson |
new simprules for abs and for things like a/b<1
|
file |
diff |
annotate
|
| Wed, 01 Sep 2004 15:04:01 +0200 |
paulson |
new "respects" syntax for quotienting
|
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, 29 Jul 2004 16:14:42 +0200 |
paulson |
removed some [iff] declarations from RealDef.thy, concerning inequalities
|
file |
diff |
annotate
|
| Sun, 11 Jul 2004 20:33:22 +0200 |
wenzelm |
local_cla/simpset_of;
|
file |
diff |
annotate
|
| Thu, 01 Jul 2004 12:29:53 +0200 |
paulson |
new treatment of binary numerals
|
file |
diff |
annotate
|
| Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
| Thu, 06 May 2004 12:43:00 +0200 |
paulson |
tidied
|
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
|
| Wed, 14 Apr 2004 14:13:05 +0200 |
kleing |
use more symbols in HTML output
|
file |
diff |
annotate
|
| Fri, 19 Mar 2004 10:51:03 +0100 |
paulson |
conversion of Hyperreal/Lim to new-style
|
file |
diff |
annotate
|
| Mon, 15 Mar 2004 10:46:19 +0100 |
paulson |
heavy tidying
|
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
|
| 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
|
| Tue, 27 Jan 2004 15:39:51 +0100 |
paulson |
replacing HOL/Real/PRat, PNat by the rational number development
|
file |
diff |
annotate
|
| Mon, 26 Jan 2004 10:34:02 +0100 |
schirmer |
* Support for raw latex output in control symbols: \<^raw...>
|
file |
diff |
annotate
|
| Fri, 09 Jan 2004 10:46:18 +0100 |
paulson |
Defining the type class "ringpower" and deleting superseded theorems for
|
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
|
| Thu, 01 Jan 2004 10:06:32 +0100 |
paulson |
tweaking of lemmas in RealDef, RealOrd
|
file |
diff |
annotate
|
| Sat, 27 Dec 2003 21:02:14 +0100 |
paulson |
re-organized numeric lemmas
|
file |
diff |
annotate
|
| Thu, 25 Dec 2003 22:48:32 +0100 |
paulson |
re-organized some hyperreal and real lemmas
|
file |
diff |
annotate
|
| Fri, 19 Dec 2003 17:13:28 +0100 |
paulson |
tidying first part of HyperArith0.ML, using generic lemmas
|
file |
diff |
annotate
|
| Thu, 18 Dec 2003 15:06:24 +0100 |
paulson |
tidied
|
file |
diff |
annotate
|
| Wed, 17 Dec 2003 16:23:52 +0100 |
paulson |
converted Hyperreal/HyperDef to Isar script
|
file |
diff |
annotate
|
| Thu, 08 Aug 2002 23:52:55 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 02 Nov 2001 17:55:24 +0100 |
paulson |
Numerals and simprocs for types real and hypreal. The abstract
|
file |
diff |
annotate
|
| Mon, 08 Oct 2001 15:23:20 +0200 |
wenzelm |
sane numerals (stage 3): provide generic "1" on all number types;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Tue, 16 Jan 2001 12:20:52 +0100 |
paulson |
renamings: real_of_nat, real_of_int -> (overloaded) real
|
file |
diff |
annotate
|
| Tue, 09 Jan 2001 15:32:27 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 05 Jan 2001 18:48:18 +0100 |
nipkow |
^^ -> ```
|
file |
diff |
annotate
|
| Thu, 04 Jan 2001 10:23:01 +0100 |
paulson |
more tidying, especially to remove real_of_posnat
|
file |
diff |
annotate
|
| Sat, 30 Dec 2000 22:03:47 +0100 |
paulson |
separation of HOL-Hyperreal from HOL-Real
|
file |
diff |
annotate
|