| Sat, 22 Dec 2001 19:46:16 +0100 |
paulson |
tweaked the standard theorems
|
file |
diff |
annotate
|
| Thu, 13 Dec 2001 12:33:23 +0100 |
paulson |
Relaxed the precondition of UN_upper_le
|
file |
diff |
annotate
|
| Tue, 06 Feb 2001 15:02:56 +0100 |
paulson |
new theorem Transset_iff_Union_subset
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 21:12:49 +0200 |
wenzelm |
tuned ML code (the_context, bind_thms(s));
|
file |
diff |
annotate
|
| Wed, 06 Sep 2000 11:47:37 +0200 |
paulson |
new Iff theorem zero_le_succ_iff
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 12:29:06 +0200 |
paulson |
new AddIffs (especially Memrel_iff)
|
file |
diff |
annotate
|
| Tue, 01 Aug 2000 18:26:34 +0200 |
paulson |
used natify with div and mod; also put in the divide-by-zero trick
|
file |
diff |
annotate
|
| Thu, 13 Jul 2000 13:00:22 +0200 |
paulson |
le_refl_iff as default rule
|
file |
diff |
annotate
|
| Wed, 28 Jun 2000 12:34:08 +0200 |
paulson |
tidying and unbatchifying
|
file |
diff |
annotate
|
| Wed, 22 Mar 2000 12:45:41 +0100 |
paulson |
tidied using new "inst" rule
|
file |
diff |
annotate
|
| Thu, 13 Jan 2000 17:36:58 +0100 |
paulson |
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
|
file |
diff |
annotate
|
| Wed, 03 Feb 1999 15:50:37 +0100 |
paulson |
tidied, with left_inverse & right_inverse as default simprules
|
file |
diff |
annotate
|
| Wed, 27 Jan 1999 10:31:31 +0100 |
paulson |
new typechecking solver for the simplifier
|
file |
diff |
annotate
|
| Thu, 10 Sep 1998 17:34:43 +0200 |
paulson |
well-formed asym rules
|
file |
diff |
annotate
|
| Fri, 14 Aug 1998 18:37:28 +0200 |
paulson |
got rid of some goal thy commands
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 14:13:18 +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
|
| Mon, 13 Jul 1998 16:43:57 +0200 |
paulson |
Huge tidy-up: removal of leading \!\!
|
file |
diff |
annotate
|
| Mon, 22 Jun 1998 17:12:27 +0200 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
| Tue, 23 Dec 1997 11:51:43 +0100 |
paulson |
Now Blast_tac works properly
|
file |
diff |
annotate
|
| Wed, 05 Nov 1997 13:14:15 +0100 |
paulson |
Ran expandshort, especially to introduce Safe_tac
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:24:13 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Mon, 29 Sep 1997 11:56:04 +0200 |
paulson |
Much tidying including step_tac -> clarify_tac or safe_tac; sometimes
|
file |
diff |
annotate
|
| Wed, 23 Apr 1997 10:54:22 +0200 |
paulson |
Conversion to use blast_tac
|
file |
diff |
annotate
|
| Wed, 09 Apr 1997 12:37:44 +0200 |
paulson |
Using Blast_tac
|
file |
diff |
annotate
|
| Tue, 04 Mar 1997 10:42:28 +0100 |
paulson |
best_tac avoids looping with change to RepFun_eqI in claset
|
file |
diff |
annotate
|
| Wed, 08 Jan 1997 15:04:27 +0100 |
paulson |
Removal of sum_cs and eq_cs
|
file |
diff |
annotate
|
| Fri, 03 Jan 1997 15:01:55 +0100 |
paulson |
Implicit simpsets and clasets for FOL and ZF
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 15:14:23 +0200 |
paulson |
Ran expandshort; used stac instead of ssubst
|
file |
diff |
annotate
|
| Tue, 26 Mar 1996 11:45:54 +0100 |
paulson |
Updated comments
|
file |
diff |
annotate
|