| Thu, 18 Jan 2001 18:39:43 +0100 |
paulson |
removed redundant proof
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 21:12:49 +0200 |
wenzelm |
tuned ML code (the_context, bind_thms(s));
|
file |
diff |
annotate
|
| Wed, 28 Jun 2000 10:56:34 +0200 |
paulson |
fixed some weak elim rules
|
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
|
| Fri, 08 Jan 1999 13:20:59 +0100 |
paulson |
removal of DO_GOAL
|
file |
diff |
annotate
|
| Mon, 28 Dec 1998 16:59:28 +0100 |
paulson |
new inductive, datatype and primrec packages, etc.
|
file |
diff |
annotate
|
| Fri, 11 Sep 1998 16:25:40 +0200 |
paulson |
fixed PROOF FAILED
|
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 12:24:04 +0200 |
paulson |
even more tidying of Goal commands
|
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
|
| Fri, 12 Dec 1997 10:46:09 +0100 |
paulson |
new blast_tac no longer works here
|
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
|
| Thu, 16 Oct 1997 13:39:20 +0200 |
wenzelm |
moved rank_Inl, rank_Inr from Epsilon.ML to Univ.ML;
|
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, 30 Apr 1997 11:42:37 +0200 |
paulson |
New theorems Pow_in_Vfrom and Pow_in_VLimit
|
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
|
| 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, 30 Jan 1996 13:42:57 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Thu, 12 Jan 1995 03:02:05 +0100 |
lcp |
Moved theorems Ord_cases_lemma and Ord_cases to Ordinal.ML
|
file |
diff |
annotate
|
| Fri, 23 Dec 1994 16:29:53 +0100 |
lcp |
Changed succ(1) to 2 in in_VLimit, two_in_univ
|
file |
diff |
annotate
|
| Fri, 16 Dec 1994 18:07:12 +0100 |
lcp |
changed useless "qed" calls for lemmas back to uses of "result",
|
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
|
| Wed, 17 Aug 1994 10:31:35 +0200 |
lcp |
ZF/Univ/Sigma_subset_univ, Transset_Pair_subset_univ: deleted
|
file |
diff |
annotate
|
| Fri, 12 Aug 1994 12:51:34 +0200 |
lcp |
installation of new inductive/datatype sections
|
file |
diff |
annotate
|
| Wed, 27 Jul 1994 15:33:42 +0200 |
lcp |
Addition of infinite branching datatypes
|
file |
diff |
annotate
|
| Tue, 26 Jul 1994 13:21:20 +0200 |
lcp |
Axiom of choice, cardinality results, etc.
|
file |
diff |
annotate
|
| Tue, 21 Jun 1994 17:20:34 +0200 |
lcp |
Addition of cardinals and order types, various tidying
|
file |
diff |
annotate
|
| Mon, 06 Dec 1993 10:57:22 +0100 |
lcp |
ZF/univ/in_Vfrom_limit: new
|
file |
diff |
annotate
|
| Thu, 07 Oct 1993 10:48:16 +0100 |
lcp |
added ~: for "not in"
|
file |
diff |
annotate
|
| Tue, 05 Oct 1993 17:15:28 +0100 |
lcp |
Retry of the previous commit (network outage)
|
file |
diff |
annotate
|
| Thu, 30 Sep 1993 10:26:38 +0100 |
lcp |
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
|
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
|