src/ZF/ZF.thy
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
Mon, 02 Dec 1996 10:22:41 +0100 wenzelm removed out-dated comment;
Tue, 06 Feb 1996 12:27:17 +0100 clasohm expanded tabs
Sat, 09 Dec 1995 13:36:11 +0100 clasohm removed quotes from consts and syntax sections
Thu, 22 Jun 1995 17:13:05 +0200 clasohm removed \...\ inside strings
Wed, 10 May 1995 08:38:52 +0200 nipkow Modified translation for pattern abstraction.
Thu, 04 May 1995 02:00:38 +0200 lcp Added pattern-matching code from CHOL/Prod.thy. Changed
Thu, 03 Nov 1994 12:35:41 +0100 lcp ZF: NEW DEFINITION OF PI(A,B)
Mon, 31 Oct 1994 18:15:24 +0100 lcp ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
Wed, 12 Oct 1994 11:09:11 +0100 wenzelm fixed infix names in print_translations;
Wed, 21 Sep 1994 15:39:02 +0200 wenzelm minor cleanup, added 'syntax' section;
Fri, 12 Aug 1994 12:51:34 +0200 lcp installation of new inductive/datatype sections
Tue, 26 Jul 1994 13:44:42 +0200 lcp Axiom of choice, cardinality results, etc.
Tue, 03 May 1994 11:28:51 +0200 lcp removal of obsolete type-declaration syntax
Mon, 25 Oct 1993 12:42:33 +0100 wenzelm added white-space;
Mon, 11 Oct 1993 12:35:00 +0100 wenzelm "The" now a binder, removed translation;
Thu, 07 Oct 1993 10:48:16 +0100 lcp added ~: for "not in"
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip