| Wed, 08 Aug 2012 12:51:20 +0200 |
wenzelm |
proper axiomatization of "mem" -- do not leave it formally unspecified;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2012 10:58:43 +0200 |
wenzelm |
clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 22:22:05 +0100 |
wenzelm |
modernized axiomatization;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 17:11:49 +0000 |
paulson |
Structured proofs concerning the square of an infinite cardinal
|
file |
diff |
annotate
|
| Tue, 06 Mar 2012 15:15:49 +0000 |
paulson |
mathematical symbols instead of ASCII
|
file |
diff |
annotate
|
| Thu, 01 Mar 2012 17:13:54 +0000 |
paulson |
Removal of obsolete ML bindings
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 20:15:02 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Thu, 11 Aug 2011 11:40:25 +0200 |
wenzelm |
redundant use of misc_legacy.ML;
|
file |
diff |
annotate
|
| Fri, 18 Feb 2011 17:03:30 +0100 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 16:44:33 +0100 |
wenzelm |
proper identifiers for consts and types;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:43:54 +0100 |
wenzelm |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 16:28:34 +0100 |
wenzelm |
prefer non-classical eliminations in Pure reasoning, notably "rule" steps;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 23:54:48 +0200 |
wenzelm |
turned eta_contract into proper configuration option;
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 14:07:09 +0200 |
wenzelm |
expanded some aliases from structure Unsynchronized;
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 12:19:27 +0200 |
haftmann |
deglobalization
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 21:38:37 +0200 |
wenzelm |
moved misc legacy stuff from OldGoals to Misc_Legacy;
|
file |
diff |
annotate
|
| Fri, 11 Jun 2010 17:14:01 +0200 |
haftmann |
avoid references to old constdefs
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 22:06:37 +0100 |
wenzelm |
numeral syntax: clarify parse trees vs. actual terms;
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 00:46:56 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 17:49:26 +0200 |
ballarin |
Lemmas added
|
file |
diff |
annotate
|
| Sun, 07 Oct 2007 21:19:31 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Wed, 03 Oct 2007 22:33:17 +0200 |
wenzelm |
avoid unnamed infixes;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 18:16:59 +0200 |
wenzelm |
tuned ML setup;
|
file |
diff |
annotate
|
| Sun, 29 Jan 2006 19:23:52 +0100 |
wenzelm |
declare atomize/defn for Ball;
|
file |
diff |
annotate
|
| Thu, 15 Dec 2005 19:42:00 +0100 |
wenzelm |
removed obsolete/unused setup_induction;
|
file |
diff |
annotate
|
| Fri, 07 Oct 2005 22:59:19 +0200 |
wenzelm |
replaced _K by dummy abstraction;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
| Tue, 08 Jun 2004 16:22:30 +0200 |
paulson |
Groups, Rings and supporting lemmas
|
file |
diff |
annotate
|
| Tue, 01 Jun 2004 12:33:50 +0200 |
wenzelm |
removed obsolete sort 'logic';
|
file |
diff |
annotate
|
| Wed, 14 Apr 2004 14:13:05 +0200 |
kleing |
use more symbols in HTML output
|
file |
diff |
annotate
|
| Fri, 10 Oct 2003 17:39:23 +0200 |
paulson |
finalconsts
|
file |
diff |
annotate
|
| Thu, 10 Jul 2003 17:14:41 +0200 |
paulson |
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
|
file |
diff |
annotate
|
| Fri, 27 Jun 2003 13:15:40 +0200 |
paulson |
Conversion of AllocBase to new-style
|
file |
diff |
annotate
|
| Wed, 15 Jan 2003 16:45:32 +0100 |
paulson |
more new-style theories
|
file |
diff |
annotate
|
| Thu, 23 May 2002 17:05:21 +0200 |
paulson |
new definition of "apply" and new simprule "beta_if"
|
file |
diff |
annotate
|
| Mon, 13 May 2002 13:22:15 +0200 |
paulson |
quotes around types
|
file |
diff |
annotate
|
| Wed, 08 May 2002 10:15:04 +0200 |
paulson |
the new predicate "relation"
|
file |
diff |
annotate
|
| Tue, 07 May 2002 14:27:54 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 15 Feb 2002 12:07:27 +0100 |
paulson |
a new definition of "restrict"
|
file |
diff |
annotate
|
| Tue, 15 Jan 2002 10:23:58 +0100 |
paulson |
split can now be unfolded even with one argument
|
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
|
| Mon, 21 May 2001 14:53:11 +0200 |
paulson |
fixed the X-symbol syntax for lambda
|
file |
diff |
annotate
|
| Fri, 30 Mar 2001 12:31:10 +0200 |
paulson |
the one-point rule for bounded quantifiers
|
file |
diff |
annotate
|
| Fri, 15 Sep 2000 00:19:52 +0200 |
wenzelm |
tuned spacing of symbols syntax;
|
file |
diff |
annotate
|
| Thu, 24 Aug 2000 11:05:20 +0200 |
paulson |
added some xsymbols, and tidied
|
file |
diff |
annotate
|
| Wed, 10 Mar 1999 10:55:12 +0100 |
wenzelm |
HTML output;
|
file |
diff |
annotate
|
| Thu, 07 Jan 1999 10:56:05 +0100 |
paulson |
if-then-else syntax for ZF
|
file |
diff |
annotate
|
| Mon, 20 Oct 1997 10:53:42 +0200 |
wenzelm |
local;
|
file |
diff |
annotate
|
| Thu, 16 Oct 1997 15:33:06 +0200 |
wenzelm |
global;
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 18:23:31 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Mon, 22 Sep 1997 17:31:57 +0200 |
wenzelm |
tuned pattern syntax;
|
file |
diff |
annotate
|
| Tue, 29 Apr 1997 17:38:02 +0200 |
wenzelm |
deactivated new symbols (not yet printable on xterm, emacs);
|
file |
diff |
annotate
|
| Tue, 29 Apr 1997 17:13:41 +0200 |
wenzelm |
added \<langle>, \<rangle> symbols syntax;
|
file |
diff |
annotate
|
| Wed, 02 Apr 1997 15:28:42 +0200 |
paulson |
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
|
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
|