src/ZF/UNITY/SubstAx.thy
Thu, 15 Mar 2012 16:35:02 +0000 paulson replacing ":" by "\<in>"
Tue, 06 Mar 2012 17:01:37 +0000 paulson More mathematical symbols for ZF examples
Sun, 15 May 2011 17:45:53 +0200 wenzelm simplified/unified method_setup/attribute_setup;
Fri, 13 May 2011 22:55:00 +0200 wenzelm proper Proof.context for classical tactics;
Sun, 28 Feb 2010 22:30:51 +0100 wenzelm more antiquotations;
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Thu, 23 Jul 2009 18:44:09 +0200 wenzelm renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
Thu, 02 Jul 2009 17:34:14 +0200 wenzelm renamed NamedThmsFun to Named_Thms;
Mon, 16 Mar 2009 18:24:30 +0100 wenzelm simplified method setup;
Fri, 15 Aug 2008 15:50:44 +0200 wenzelm Args.name_source(_position) for proper position information;
Mon, 16 Jun 2008 22:13:39 +0200 wenzelm pervasive RuleInsts;
Sat, 14 Jun 2008 23:19:51 +0200 wenzelm proper context for tactics derived from res_inst_tac;
Wed, 26 Mar 2008 22:40:10 +0100 wenzelm removed legacy ML bindings;
Sun, 07 Oct 2007 21:19:31 +0200 wenzelm modernized specifications;
Sun, 29 Jul 2007 14:30:07 +0200 wenzelm replaced program_defs_ref by proper context data (via attribute "program");
Sat, 21 Jul 2007 23:25:00 +0200 wenzelm tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
Thu, 08 Dec 2005 20:15:41 +0100 wenzelm Cla.swap;
Mon, 28 Mar 2005 16:19:56 +0200 paulson conversion of UNITY to Isar scripts
Thu, 15 Nov 2001 15:07:16 +0100 ehmety *** empty log message ***
Wed, 08 Aug 2001 14:33:10 +0200 paulson new ZF/UNITY theory
less more (0) tip