| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 21:31:28 +0200 |
nipkow |
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
|
file |
diff |
annotate
|
| Wed, 02 Jul 2008 07:11:57 +0200 |
haftmann |
cleaned up some code generator configuration
|
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
|
| Mon, 20 Aug 2007 19:52:52 +0200 |
huffman |
remove int_of_nat
|
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
|
| Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Mon, 11 Jun 2007 07:10:06 +0200 |
huffman |
remove references to constant int::nat=>int
|
file |
diff |
annotate
|
| Sat, 19 May 2007 04:52:24 +0200 |
huffman |
remove dependence on Hilbert_Choice.thy
|
file |
diff |
annotate
|
| Fri, 18 May 2007 16:13:07 +0200 |
huffman |
avoid using real_mult_inverse_left; cleaned up
|
file |
diff |
annotate
|
| Thu, 17 May 2007 21:51:32 +0200 |
huffman |
avoid using redundant lemmas from RealDef.thy
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
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
|
| Sun, 11 Jun 2006 22:45:53 +0200 |
wenzelm |
fixed subst step;
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 23:22:29 +0200 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 20:47:00 +0200 |
wenzelm |
some structured proofs on completeness;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 17:16:52 +0200 |
wenzelm |
accomodate change of real_of_XXX;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 20:02:54 +0200 |
avigad |
fixed typos in theorem names
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 19:49:07 +0200 |
avigad |
Additions to the Real (and Hyperreal) libraries:
|
file |
diff |
annotate
|
| Mon, 21 Feb 2005 15:04:10 +0100 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
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
|
| Thu, 22 Apr 2004 10:45:56 +0200 |
paulson |
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
|
file |
diff |
annotate
|
| Fri, 19 Mar 2004 10:50:06 +0100 |
paulson |
removed redundant thms
|
file |
diff |
annotate
|
| Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
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, 24 Jul 2000 23:59:32 +0200 |
wenzelm |
changed deps;
|
file |
diff |
annotate
|
| Thu, 19 Aug 1999 18:36:41 +0200 |
paulson |
real literals using binary arithmetic
|
file |
diff |
annotate
|
| Mon, 16 Aug 1999 18:41:32 +0200 |
paulson |
inserted Id: lines
|
file |
diff |
annotate
|
| Thu, 25 Jun 1998 13:57:34 +0200 |
paulson |
Installation of target HOL-Real
|
file |
diff |
annotate
|