src/FOL/IFOL.thy
Mon, 06 Sep 2010 19:13:10 +0200 wenzelm more antiquotations;
Wed, 18 Aug 2010 12:26:48 +0200 haftmann deglobalization
Wed, 28 Apr 2010 12:07:52 +0200 wenzelm renamed command 'defaultsort' to 'default_sort';
Mon, 01 Mar 2010 13:42:31 +0100 haftmann merged
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Sun, 28 Feb 2010 22:30:51 +0100 wenzelm more antiquotations;
Mon, 08 Feb 2010 21:28:27 +0100 wenzelm modernized some syntax translations;
Sun, 01 Nov 2009 15:44:26 +0100 wenzelm modernized structure Context_Rules;
Fri, 24 Jul 2009 18:58:58 +0200 wenzelm renamed functor ProjectRuleFun to Project_Rule;
Sat, 30 May 2009 12:52:57 +0200 wenzelm modernized method setup;
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Sat, 28 Feb 2009 14:52:21 +0100 wenzelm moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
Sat, 28 Feb 2009 14:02:12 +0100 wenzelm moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
Thu, 20 Nov 2008 00:03:47 +0100 wenzelm Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
Tue, 28 Oct 2008 11:03:07 +0100 ballarin Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
Fri, 24 Oct 2008 17:48:33 +0200 haftmann subst is a proper axiom again
Wed, 11 Jun 2008 18:01:11 +0200 wenzelm removed obsolete/unused pred_congs;
Wed, 11 Jun 2008 15:41:57 +0200 wenzelm tuned comments;
Sun, 18 May 2008 17:03:16 +0200 wenzelm setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
Tue, 08 Apr 2008 18:30:40 +0200 krauss Generic conversion and tactic "atomize_elim" to convert elimination rules
Sat, 15 Mar 2008 22:07:25 +0100 wenzelm added lemmas from simpdata.ML;
Thu, 04 Oct 2007 14:42:47 +0200 wenzelm moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
Tue, 31 Jul 2007 21:19:18 +0200 wenzelm moved classical tools from theory IFOL to FOL;
Thu, 14 Jun 2007 23:04:36 +0200 wenzelm tuned proofs: avoid implicit prems;
Thu, 31 May 2007 20:55:29 +0200 wenzelm moved IsaPlanner from Provers to Tools;
Thu, 31 May 2007 14:34:06 +0200 wenzelm proper loading of ML files;
Fri, 11 May 2007 00:43:45 +0200 wenzelm tuned proofs;
Sat, 20 Jan 2007 14:09:27 +0100 wenzelm tuned ML setup;
Sun, 26 Nov 2006 23:43:53 +0100 wenzelm converted legacy ML scripts;
Sun, 26 Nov 2006 18:07:16 +0100 wenzelm updated (binder) syntax/notation;
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Tue, 07 Nov 2006 11:47:57 +0100 wenzelm renamed 'const_syntax' to 'notation';
Thu, 01 Jun 2006 21:14:54 +0200 wenzelm lemmas strip;
Sat, 20 May 2006 23:36:49 +0200 wenzelm removed obsolete 'finalconsts';
Tue, 16 May 2006 21:33:01 +0200 wenzelm tuned concrete syntax -- abbreviation/const_syntax;
Sun, 09 Apr 2006 18:51:13 +0200 wenzelm tuned syntax/abbreviations;
Sat, 08 Apr 2006 22:51:06 +0200 wenzelm refined 'abbreviation';
Wed, 22 Feb 2006 22:18:31 +0100 wenzelm not_equal: replaced syntax translation by abbreviation;
Tue, 31 Jan 2006 00:43:14 +0100 wenzelm declare defn rules;
Fri, 27 Jan 2006 19:05:24 +0100 wenzelm added atomize_iff;
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Fri, 30 Dec 2005 16:56:57 +0100 wenzelm fixed final_consts;
Thu, 22 Dec 2005 00:29:14 +0100 wenzelm structure ProjectRule;
Thu, 29 Sep 2005 00:58:55 +0200 wenzelm more finalconsts;
Fri, 23 Sep 2005 00:11:10 +0200 nipkow renamed rules to iprover
Tue, 06 Sep 2005 16:59:51 +0200 wenzelm avoid old-style infixes;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Tue, 31 May 2005 11:53:12 +0200 wenzelm tuned;
Sun, 22 May 2005 16:51:07 +0200 wenzelm Simplifier already setup in Pure;
Tue, 01 Feb 2005 18:01:57 +0100 paulson the new subst tactic, by Lucas Dixon
Tue, 07 Dec 2004 11:31:14 +0100 paulson proof of subst by S Merz
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
Thu, 16 Oct 2003 10:31:40 +0200 paulson partial conversion to Isar scripts
Wed, 15 Jan 2003 16:44:21 +0100 paulson moving "let" from ZF to FOL
Wed, 31 Jul 2002 14:34:08 +0200 paulson new theorem eq_commute
Mon, 25 Feb 2002 20:48:14 +0100 wenzelm clarified syntax of ``long'' statements: fixes/assumes/shows;
Tue, 12 Feb 2002 20:25:58 +0100 wenzelm tuned;
Tue, 08 Jan 2002 00:03:42 +0100 wenzelm syntax "_not_equal";
less more (0) -60 tip