| 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
|