src/FOL/IFOL.thy
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";
Wed, 05 Dec 2001 03:00:39 +0100 wenzelm sym declarations;
Tue, 04 Dec 2001 02:00:14 +0100 wenzelm renamed RuleContext to ContextRules;
Mon, 03 Dec 2001 21:03:06 +0100 wenzelm setup "rules" method;
Fri, 09 Nov 2001 00:09:47 +0100 wenzelm eliminated old "symbols" syntax, use "xsymbols" instead;
Fri, 02 Nov 2001 22:01:07 +0100 wenzelm transitive declared in Pure;
Sun, 28 Oct 2001 21:10:47 +0100 wenzelm equal_intr_rule already declared in Pure;
Fri, 26 Oct 2001 23:59:13 +0200 wenzelm atomize_conj;
Sat, 20 Oct 2001 20:18:45 +0200 wenzelm calculational rules moved from FOL to IFOL;
Sun, 14 Oct 2001 22:15:07 +0200 wenzelm moved rulify to ObjectLogic;
Sun, 14 Oct 2001 19:59:15 +0200 wenzelm judgment Trueprop;
Fri, 12 Oct 2001 12:11:39 +0200 wenzelm declare impE iffD1 iffD2 ad elim of Pure;
Thu, 04 Oct 2001 15:28:00 +0200 wenzelm atomize stuff from theory FOL;
Thu, 07 Sep 2000 20:47:54 +0200 wenzelm updated setup;
Fri, 04 Aug 2000 22:55:08 +0200 wenzelm setup hypsubst_setup;
Wed, 25 Aug 1999 20:45:19 +0200 wenzelm proper bootstrap of IFOL/FOL theories and packages;
Wed, 10 Mar 1999 10:55:12 +0100 wenzelm HTML output;
Fri, 11 Dec 1998 18:56:30 +0100 oheimb added new print_mode "xsymbols" for extended symbol support
Wed, 29 Apr 1998 11:29:39 +0200 wenzelm tuned setup;
Sat, 04 Apr 1998 12:28:39 +0200 wenzelm replaced thy_data by thy_setup;
Mon, 03 Nov 1997 12:26:45 +0100 wenzelm added simpset thy_data;
Mon, 20 Oct 1997 10:38:36 +0200 wenzelm local;
Thu, 16 Oct 1997 15:33:06 +0200 wenzelm global;
Fri, 10 Oct 1997 15:52:12 +0200 wenzelm fixed dots;
Tue, 10 Dec 1996 13:03:44 +0100 wenzelm fixed pris of binder syntax;
Wed, 27 Nov 1996 16:42:48 +0100 wenzelm symbol names changes;
Mon, 18 Nov 1996 17:33:35 +0100 wenzelm added symbolfont syntax;
Tue, 07 Nov 1995 12:58:17 +0100 clasohm removed quotes from types in consts section
Thu, 05 Oct 1995 14:45:54 +0100 clasohm corrected title
Tue, 07 Mar 1995 13:15:25 +0100 lcp Moved declaration of ~= to a syntax section
Thu, 17 Mar 1994 11:24:31 +0100 clasohm adapted type definition to new syntax
Mon, 25 Oct 1993 12:32:53 +0100 wenzelm added white-space;
Thu, 07 Oct 1993 09:47:47 +0100 lcp ifol.thy: added ~= for "not equals"
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip