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