| Tue, 02 Aug 2005 19:47:12 +0200 |
wenzelm |
simprocs: Simplifier.inherit_bounds;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Wed, 14 Apr 2004 14:13:05 +0200 |
kleing |
use more symbols in HTML output
|
file |
diff |
annotate
|
| Thu, 06 Feb 2003 11:01:05 +0100 |
paulson |
changed ** to ## to avoid conflict with new comment syntax
|
file |
diff |
annotate
|
| Tue, 01 Oct 2002 13:26:10 +0200 |
paulson |
Numerous cosmetic changes, prompted by the new simplifier
|
file |
diff |
annotate
|
| Tue, 06 Aug 2002 11:22:05 +0200 |
wenzelm |
sane interface for simprocs;
|
file |
diff |
annotate
|
| Tue, 16 Jul 2002 16:28:49 +0200 |
paulson |
tweaked definition of setclass
|
file |
diff |
annotate
|
| Wed, 10 Jul 2002 16:54:07 +0200 |
paulson |
Fixed quantified variable name preservation for ball and bex (bounded quants)
|
file |
diff |
annotate
|
| Fri, 05 Jul 2002 11:39:52 +0200 |
paulson |
fixed precedences of **
|
file |
diff |
annotate
|
| Thu, 04 Jul 2002 16:59:54 +0200 |
paulson |
Constructible: some separation axioms
|
file |
diff |
annotate
|
| Thu, 04 Jul 2002 10:50:24 +0200 |
paulson |
miniscoping for class-bounded quantifiers (rall and rex)
|
file |
diff |
annotate
|
| Fri, 28 Jun 2002 11:24:36 +0200 |
paulson |
added class quantifiers
|
file |
diff |
annotate
|
| Mon, 24 Jun 2002 11:59:14 +0200 |
paulson |
moving some results around
|
file |
diff |
annotate
|
| 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
|