Fri, 25 Jan 2008 14:54:41 +0100 |
haftmann |
improved code theorem setup
|
file |
diff |
annotate
|
Thu, 10 Jan 2008 19:09:21 +0100 |
berghofe |
New interface for test data generators.
|
file |
diff |
annotate
|
Wed, 02 Jan 2008 15:14:02 +0100 |
haftmann |
splitted class uminus from class minus
|
file |
diff |
annotate
|
Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
Wed, 05 Dec 2007 16:54:50 +0100 |
obua |
instance int,real :: lordered_ring
|
file |
diff |
annotate
|
Thu, 29 Nov 2007 17:08:26 +0100 |
haftmann |
instance command as rudimentary class target
|
file |
diff |
annotate
|
Tue, 06 Nov 2007 08:47:25 +0100 |
haftmann |
renamed lordered_*_* to lordered_*_add_*; further localization
|
file |
diff |
annotate
|
Tue, 23 Oct 2007 23:27:23 +0200 |
nipkow |
went back to >0
|
file |
diff |
annotate
|
Sun, 21 Oct 2007 22:33:35 +0200 |
nipkow |
More changes from >0 to ~=0::nat
|
file |
diff |
annotate
|
Sun, 21 Oct 2007 14:53:44 +0200 |
nipkow |
Eliminated most of the neq0_conv occurrences. As a result, many
|
file |
diff |
annotate
|
Sat, 20 Oct 2007 12:09:33 +0200 |
chaieb |
fixed proofs
|
file |
diff |
annotate
|
Tue, 18 Sep 2007 16:08:00 +0200 |
wenzelm |
simplified type int (eliminated IntInf.int, integer);
|
file |
diff |
annotate
|
Tue, 18 Sep 2007 07:36:14 +0200 |
haftmann |
renamed constructor RealC to Ratreal
|
file |
diff |
annotate
|
Thu, 06 Sep 2007 11:39:43 +0200 |
berghofe |
New code generator setup (taken from Library/Executable_Real.thy,
|
file |
diff |
annotate
|
Sat, 01 Sep 2007 01:21:48 +0200 |
nipkow |
final(?) iteration of sgn saga.
|
file |
diff |
annotate
|
Thu, 09 Aug 2007 15:52:53 +0200 |
haftmann |
adaptions for code generation
|
file |
diff |
annotate
|
Tue, 31 Jul 2007 00:56:26 +0200 |
wenzelm |
arith method setup: proper context;
|
file |
diff |
annotate
|
Fri, 20 Jul 2007 14:28:01 +0200 |
haftmann |
split class abs from class minus
|
file |
diff |
annotate
|
Sun, 24 Jun 2007 20:55:41 +0200 |
nipkow |
tuned and used field_simps
|
file |
diff |
annotate
|
Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
Wed, 20 Jun 2007 17:28:55 +0200 |
huffman |
remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
|
file |
diff |
annotate
|
Wed, 20 Jun 2007 05:18:39 +0200 |
huffman |
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
|
file |
diff |
annotate
|
Thu, 07 Jun 2007 04:33:15 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
Thu, 07 Jun 2007 03:45:56 +0200 |
huffman |
remove references to preal-specific theorems
|
file |
diff |
annotate
|
Thu, 07 Jun 2007 03:11:31 +0200 |
huffman |
define (1::preal); clean up instance declarations
|
file |
diff |
annotate
|
Sat, 19 May 2007 13:41:13 +0200 |
nipkow |
added code generation based on Isabelle's rat type.
|
file |
diff |
annotate
|
Mon, 14 May 2007 18:48:24 +0200 |
huffman |
move lemmas to RealPow.thy; tuned proofs
|
file |
diff |
annotate
|
Mon, 14 May 2007 09:33:18 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
Mon, 14 May 2007 08:15:13 +0200 |
huffman |
cleaned up
|
file |
diff |
annotate
|
Fri, 16 Mar 2007 21:32:12 +0100 |
haftmann |
added lattice definitions
|
file |
diff |
annotate
|
Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
Sat, 16 Sep 2006 19:12:03 +0200 |
huffman |
define new constant of_real for class real_algebra_1;
|
file |
diff |
annotate
|
Wed, 06 Sep 2006 13:48:02 +0200 |
haftmann |
got rid of Numeral.bin type
|
file |
diff |
annotate
|
Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic 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
|
Sun, 12 Feb 2006 12:29:01 +0100 |
kleing |
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
|
file |
diff |
annotate
|
Mon, 01 Aug 2005 19:20:26 +0200 |
wenzelm |
simprocs: Simplifier.inherit_bounds;
|
file |
diff |
annotate
|
Tue, 19 Jul 2005 17:24:09 +0200 |
avigad |
added list of theorem changes to NEWS
|
file |
diff |
annotate
|
Wed, 13 Jul 2005 19:49:07 +0200 |
avigad |
Additions to the Real (and Hyperreal) libraries:
|
file |
diff |
annotate
|
Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
Wed, 04 May 2005 10:42:43 +0200 |
nipkow |
fixed lin.arith
|
file |
diff |
annotate
|
Mon, 21 Feb 2005 19:23:46 +0100 |
nipkow |
more fine tuniung
|
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:57:41 +0200 |
paulson |
removal of more iff-rules from RealDef.thy
|
file |
diff |
annotate
|
Thu, 29 Jul 2004 16:14:42 +0200 |
paulson |
removed some [iff] declarations from RealDef.thy, concerning inequalities
|
file |
diff |
annotate
|
Mon, 26 Jul 2004 17:34:52 +0200 |
paulson |
converting Hyperreal/Transcendental to Isar script
|
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, 18 May 2004 10:01:44 +0200 |
obua |
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
|
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
|
Tue, 30 Mar 2004 11:25:14 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
Thu, 25 Mar 2004 10:31:25 +0100 |
paulson |
new treatment of equivalence classes
|
file |
diff |
annotate
|
Fri, 19 Mar 2004 10:50:06 +0100 |
paulson |
removed redundant thms
|
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
|