Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
Thu, 07 Jun 2007 03:11:31 +0200 |
huffman |
define (1::preal); clean up instance declarations
|
file |
diff |
annotate
|
Thu, 07 Jun 2007 01:44:35 +0200 |
huffman |
instance preal :: ordered_cancel_ab_semigroup_add
|
file |
diff |
annotate
|
Sun, 15 Apr 2007 23:25:52 +0200 |
wenzelm |
read prop as prop, not term;
|
file |
diff |
annotate
|
Tue, 20 Mar 2007 15:52:40 +0100 |
haftmann |
added instance for lattice
|
file |
diff |
annotate
|
Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
Sat, 09 Sep 2006 18:28:42 +0200 |
huffman |
cleaned up
|
file |
diff |
annotate
|
Fri, 02 Jun 2006 23:22:29 +0200 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
Mon, 19 Dec 2005 09:19:08 +0100 |
nipkow |
fixed proof
|
file |
diff |
annotate
|
Sat, 17 Dec 2005 01:58:41 +0100 |
wenzelm |
simp del: empty_Collect_eq;
|
file |
diff |
annotate
|
Mon, 21 Nov 2005 11:14:11 +0100 |
paulson |
tweak
|
file |
diff |
annotate
|
Thu, 15 Sep 2005 23:16:04 +0200 |
huffman |
add header
|
file |
diff |
annotate
|
Tue, 12 Jul 2005 17:56:03 +0200 |
avigad |
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
|
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
|
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
|
Fri, 16 Jul 2004 17:32:34 +0200 |
nipkow |
Corrected TeX problem.
|
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
|
Sat, 01 May 2004 22:01:57 +0200 |
wenzelm |
tuned instance statements;
|
file |
diff |
annotate
|
Tue, 13 Apr 2004 07:48:32 +0200 |
kleing |
hence -> from calculation have
|
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
|
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
|
Thu, 05 Feb 2004 10:45:28 +0100 |
paulson |
tidying up, especially the Complex numbers
|
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
|
Thu, 01 Jan 2004 21:47:07 +0100 |
paulson |
conversion of Real/PReal to Isar script;
|
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, 11 Oct 1999 10:52:51 +0200 |
paulson |
replaced {x. True} by UNIV to work with the new simprule, Collect_const
|
file |
diff |
annotate
|
Mon, 16 Aug 1999 18:41:32 +0200 |
paulson |
inserted Id: lines
|
file |
diff |
annotate
|
Fri, 23 Jul 1999 17:29:12 +0200 |
paulson |
heavily revised by Jacques: coercions have alphabetic names;
|
file |
diff |
annotate
|
Thu, 25 Jun 1998 13:57:34 +0200 |
paulson |
Installation of target HOL-Real
|
file |
diff |
annotate
|