| Thu, 01 Jan 2004 21:47:07 +0100 |
paulson |
conversion of Real/PReal to Isar script;
|
file |
diff |
annotate
|
| Wed, 31 Jul 2002 16:10:24 +0200 |
nipkow |
added mk_left_commute to HOL.thy and used it "everywhere"
|
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
|
| 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
|
| Wed, 03 Oct 2001 20:54:16 +0200 |
wenzelm |
tuned parentheses in relational expressions;
|
file |
diff |
annotate
|
| Mon, 06 Aug 2001 13:43:24 +0200 |
nipkow |
turned translation for 1::nat into def.
|
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
|
| Sat, 30 Dec 2000 22:13:18 +0100 |
paulson |
tidying, and separation of HOL-Hyperreal from HOL-Real
|
file |
diff |
annotate
|
| Tue, 17 Oct 2000 10:23:16 +0200 |
paulson |
restoration of "equalityI"; renaming of contrapos rules
|
file |
diff |
annotate
|
| Fri, 15 Sep 2000 12:39:57 +0200 |
paulson |
renamed (most of...) the select rules
|
file |
diff |
annotate
|
| Mon, 24 Jul 2000 23:58:19 +0200 |
wenzelm |
avoid referencing thy value;
|
file |
diff |
annotate
|
| Wed, 19 Jul 2000 12:33:19 +0200 |
paulson |
changed / to // for quotienting; general tidying
|
file |
diff |
annotate
|
| Sun, 16 Jul 2000 20:57:34 +0200 |
wenzelm |
use pair_tac;
|
file |
diff |
annotate
|
| Thu, 22 Jun 2000 23:04:34 +0200 |
wenzelm |
bind_thm(s);
|
file |
diff |
annotate
|
| Wed, 07 Jun 2000 12:14:18 +0200 |
paulson |
First round of changes, towards installation of simprocs
|
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
|
| Fri, 27 Aug 1999 15:43:53 +0200 |
paulson |
tidied, allowing pattern-matching in defs of prat_add and prat_mult
|
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
|
| Wed, 23 Sep 1998 10:03:32 +0200 |
paulson |
deleted needless parentheses
|
file |
diff |
annotate
|
| Thu, 10 Sep 1998 17:29:56 +0200 |
paulson |
well-formed asym rules; misc. tidying
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 14:19:02 +0200 |
paulson |
More tidying and removal of "\!\!... from Goal commands
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 10:15:13 +0200 |
paulson |
Removal of leading "\!\!..." from most Goal commands
|
file |
diff |
annotate
|
| Thu, 25 Jun 1998 13:57:34 +0200 |
paulson |
Installation of target HOL-Real
|
file |
diff |
annotate
|