src/ZF/ZF.thy
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Thu, 03 Jan 2019 21:15:52 +0100 wenzelm isabelle update -u mixfix_cartouches;
Sun, 24 Jun 2018 15:57:48 +0200 wenzelm simplified ZF theory names (in contrast to 6a0801279f4c): session-qualification already achieves disjointness;
Wed, 12 Apr 2017 13:48:07 +0200 wenzelm merged
Mon, 10 Apr 2017 11:50:15 +0200 wenzelm tuned text;
Sun, 09 Apr 2017 20:44:35 +0200 wenzelm clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
Tue, 04 Apr 2017 23:21:16 +0200 wenzelm allow to load this into "isabelle jedit -l HOL";
Fri, 16 Sep 2016 21:28:09 +0200 wenzelm more symbols;
Tue, 12 Jan 2016 00:18:43 +0100 wenzelm clarified axiomatization versus definitions;
Wed, 30 Dec 2015 17:45:18 +0100 wenzelm clarified syntax;
Wed, 30 Dec 2015 17:38:57 +0100 wenzelm clarified print modes;
Mon, 07 Dec 2015 10:23:50 +0100 wenzelm isabelle update_cartouches -c -t;
Fri, 09 Oct 2015 20:26:03 +0200 wenzelm discontinued specific HTML syntax;
Thu, 23 Jul 2015 14:25:05 +0200 wenzelm isabelle update_cartouches;
Sun, 02 Nov 2014 16:39:54 +0100 wenzelm modernized header;
Mon, 10 Feb 2014 17:20:11 +0100 wenzelm prefer vacuous definitional type classes over axiomatic ones;
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
less more (0) -60 tip