| Mon, 21 May 2001 14:36:24 +0200 |
paulson |
X-symbols for set theory
|
file |
diff |
annotate
|
| Tue, 01 Aug 2000 15:28:21 +0200 |
paulson |
natify, a coercion to reduce the number of type constraints in arithmetic
|
file |
diff |
annotate
|
| Mon, 07 Feb 2000 15:14:02 +0100 |
paulson |
tidied some proofs
|
file |
diff |
annotate
|
| Tue, 07 Sep 1999 10:40:58 +0200 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
| Fri, 29 Jan 1999 17:08:20 +0100 |
paulson |
expandshort
|
file |
diff |
annotate
|
| Wed, 27 Jan 1999 15:58:22 +0100 |
paulson |
automatic insertion of datatype intr rules into claset
|
file |
diff |
annotate
|
| Wed, 27 Jan 1999 10:31:31 +0100 |
paulson |
new typechecking solver for the simplifier
|
file |
diff |
annotate
|
| Wed, 13 Jan 1999 11:57:09 +0100 |
paulson |
datatype package improvements
|
file |
diff |
annotate
|
| Fri, 08 Jan 1999 13:20:59 +0100 |
paulson |
removal of DO_GOAL
|
file |
diff |
annotate
|
| Thu, 07 Jan 1999 18:30:55 +0100 |
paulson |
ZF: the natural numbers as a datatype
|
file |
diff |
annotate
|
| Wed, 06 Jan 1999 13:24:33 +0100 |
paulson |
induct_tac and exhaust_tac
|
file |
diff |
annotate
|
| Mon, 28 Dec 1998 16:52:51 +0100 |
paulson |
Needs separate theory Primrec_defs due to new inductive defs package
|
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:13:09 +0200 |
wenzelm |
isatool fixgoal;
|
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
|
| Fri, 10 Oct 1997 18:23:31 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Mon, 26 May 1997 12:25:15 +0200 |
paulson |
Slight simplifications
|
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
|
| Fri, 03 Jan 1997 15:01:55 +0100 |
paulson |
Implicit simpsets and clasets for FOL and ZF
|
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
|
| Fri, 12 Aug 1994 12:28:46 +0200 |
lcp |
installation of new inductive/datatype sections
|
file |
diff |
annotate
|