| Wed, 13 Feb 2002 10:44:39 +0100 |
paulson |
tidied. no more special simpset (super_ss)
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 21:12:49 +0200 |
wenzelm |
tuned ML code (the_context, bind_thms(s));
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 17:36:37 +0200 |
paulson |
a number of new theorems
|
file |
diff |
annotate
|
| Wed, 28 Jun 2000 12:34:08 +0200 |
paulson |
tidying and unbatchifying
|
file |
diff |
annotate
|
| Wed, 28 Jun 2000 10:56:34 +0200 |
paulson |
fixed some weak elim rules
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 19:11:07 +0200 |
nipkow |
Mod because of new solver interface.
|
file |
diff |
annotate
|
| Wed, 13 Jan 1999 11:57:09 +0100 |
paulson |
datatype package improvements
|
file |
diff |
annotate
|
| Thu, 10 Sep 1998 17:23:51 +0200 |
paulson |
New theorem wf_not_sym and well-formed wf_asym
|
file |
diff |
annotate
|
| Fri, 14 Aug 1998 18:37:28 +0200 |
paulson |
got rid of some goal thy commands
|
file |
diff |
annotate
|
| Thu, 06 Aug 1998 10:38:57 +0200 |
paulson |
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 14:13:18 +0200 |
paulson |
More tidying and removal of "\!\!... from 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
|
| Mon, 05 Jan 1998 10:47:10 +0100 |
paulson |
Now calls Blast_tac more often
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:24:13 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Wed, 23 Apr 1997 10:54:22 +0200 |
paulson |
Conversion to use blast_tac
|
file |
diff |
annotate
|
| Sat, 15 Feb 1997 17:52:31 +0100 |
oheimb |
reflecting my recent changes of the simplifier and classical reasoner
|
file |
diff |
annotate
|
| Tue, 07 Jan 1997 12:37:07 +0100 |
paulson |
Default rewrite rules for quantification over Collect(A,P)
|
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, 30 Jan 1996 13:42:57 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Wed, 14 Dec 1994 11:41:49 +0100 |
clasohm |
added bind_thm for theorems defined by "standard ..."
|
file |
diff |
annotate
|
| Wed, 07 Dec 1994 13:12:04 +0100 |
clasohm |
added qed and qed_goal[w]
|
file |
diff |
annotate
|
| Thu, 28 Jul 1994 12:44:40 +0200 |
lcp |
ZF/WF/wf_induct: streamlined proof
|
file |
diff |
annotate
|
| Tue, 26 Jul 1994 13:44:42 +0200 |
lcp |
Axiom of choice, cardinality results, etc.
|
file |
diff |
annotate
|
| Wed, 29 Jun 1994 12:13:03 +0200 |
clasohm |
added parentheses made necessary by new constrain precedence
|
file |
diff |
annotate
|
| Thu, 23 Jun 1994 17:38:12 +0200 |
lcp |
modifications for cardinal arithmetic
|
file |
diff |
annotate
|
| Tue, 21 Jun 1994 17:20:34 +0200 |
lcp |
Addition of cardinals and order types, various tidying
|
file |
diff |
annotate
|
| Fri, 17 Sep 1993 16:16:38 +0200 |
lcp |
Installation of new simplifier for ZF. Deleted all congruence rules not
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|