| 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
|
| Sat, 30 Dec 2000 22:13:18 +0100 |
paulson |
tidying, and separation of HOL-Hyperreal from HOL-Real
|
file |
diff |
annotate
|
| Mon, 23 Oct 2000 15:20:15 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Tue, 17 Oct 2000 10:21:12 +0200 |
paulson |
renaming of contrapos rules
|
file |
diff |
annotate
|
| Thu, 12 Oct 2000 13:01:19 +0200 |
nipkow |
induct -> lfp_induct
|
file |
diff |
annotate
|
| Wed, 11 Oct 2000 09:09:06 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 30 Aug 2000 16:29:21 +0200 |
nipkow |
introduced induct_thm_tac
|
file |
diff |
annotate
|
| Thu, 17 Aug 2000 12:00:23 +0200 |
paulson |
tidied & updated proofs, deleting some unused ones
|
file |
diff |
annotate
|
| Mon, 24 Jul 2000 23:51:46 +0200 |
wenzelm |
avoid referencing thy value;
|
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
|
| Fri, 12 May 2000 15:14:35 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Wed, 10 May 2000 22:34:30 +0200 |
wenzelm |
fixed theory deps;
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 17:29:00 +0200 |
wenzelm |
tuned;
|
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
|
| Fri, 23 Jul 1999 17:29:12 +0200 |
paulson |
heavily revised by Jacques: coercions have alphabetic names;
|
file |
diff |
annotate
|
| Sat, 09 Jan 1999 15:24:11 +0100 |
nipkow |
Refined arith tactic.
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 20:44:34 +0200 |
oheimb |
corrected auto_tac (applications of unsafe wrappers)
|
file |
diff |
annotate
|
| Thu, 01 Oct 1998 18:18:01 +0200 |
paulson |
Revised version with Abelian group simprocs
|
file |
diff |
annotate
|
| Thu, 10 Sep 1998 17:29:56 +0200 |
paulson |
well-formed asym rules; misc. tidying
|
file |
diff |
annotate
|
| Thu, 06 Aug 1998 12:45:28 +0200 |
nipkow |
Removed duplicate thms (see comment to Arith.ML)
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:19:38 +0200 |
berghofe |
Adapted to new datatype package.
|
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
|