| Thu, 23 May 2002 17:05:21 +0200 | paulson | new definition of "apply" and new simprule "beta_if" | file | diff | annotate |
| Wed, 22 May 2002 19:34:01 +0200 | paulson | more tidying | file | diff | annotate |
| Wed, 22 May 2002 18:11:57 +0200 | paulson | tidying up | file | diff | annotate |
| Wed, 22 May 2002 17:25:40 +0200 | paulson | tidied | file | diff | annotate |
| Tue, 21 May 2002 18:25:28 +0200 | paulson | conversion of OrdQuant.ML to Isar | file | diff | annotate |
| Fri, 17 May 2002 16:54:25 +0200 | paulson | New theorems from Constructible, and moving some Isar material from Main | file | diff | annotate |
| Wed, 15 May 2002 10:42:32 +0200 | paulson | better simplification of trivial existential equalities | file | diff | annotate |
| Wed, 08 May 2002 10:12:57 +0200 | paulson | new lemmas | file | diff | annotate |
| Mon, 21 Jan 2002 14:47:55 +0100 | paulson | new simprules and classical rules | file | diff | annotate |
| Mon, 21 Jan 2002 11:25:45 +0100 | paulson | lexical tidying | file | diff | annotate |
| Tue, 15 Jan 2002 10:24:20 +0100 | paulson | now [rule_format] knows about ospec | file | diff | annotate |
| Tue, 08 Jan 2002 16:09:09 +0100 | paulson | Added some simprules proofs. | file | diff | annotate |
| Thu, 03 Jan 2002 17:01:59 +0100 | paulson | Some new theorems for ordinals | file | diff | annotate |
| Wed, 19 Dec 2001 11:13:27 +0100 | paulson | separation of the AC part of Main into Main_ZFC, plus a few new lemmas | file | diff | annotate |
| Fri, 09 Nov 2001 00:09:47 +0100 | wenzelm | eliminated old "symbols" syntax, use "xsymbols" instead; | file | diff | annotate |
| Tue, 12 Jan 1999 15:17:37 +0100 | wenzelm | eliminated global/local names; | file | diff | annotate |
| Mon, 20 Oct 1997 10:53:42 +0200 | wenzelm | local; | file | diff | annotate |
| Fri, 17 Oct 1997 17:40:02 +0200 | wenzelm | global; | file | diff | annotate |
| Thu, 23 Jan 1997 12:42:07 +0100 | wenzelm | added symbols syntax; | file | diff | annotate |
| Fri, 03 Jan 1997 15:01:55 +0100 | paulson | Implicit simpsets and clasets for FOL and ZF | file | diff | annotate |