| Thu, 20 Nov 2008 00:03:47 +0100 |
wenzelm |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
file |
diff |
annotate
|
| Tue, 28 Oct 2008 11:03:07 +0100 |
ballarin |
Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
|
file |
diff |
annotate
|
| Fri, 24 Oct 2008 17:48:33 +0200 |
haftmann |
subst is a proper axiom again
|
file |
diff |
annotate
|
| Wed, 11 Jun 2008 18:01:11 +0200 |
wenzelm |
removed obsolete/unused pred_congs;
|
file |
diff |
annotate
|
| Wed, 11 Jun 2008 15:41:57 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 17:03:16 +0200 |
wenzelm |
setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2008 18:30:40 +0200 |
krauss |
Generic conversion and tactic "atomize_elim" to convert elimination rules
|
file |
diff |
annotate
|
| Sat, 15 Mar 2008 22:07:25 +0100 |
wenzelm |
added lemmas from simpdata.ML;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 14:42:47 +0200 |
wenzelm |
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 21:19:18 +0200 |
wenzelm |
moved classical tools from theory IFOL to FOL;
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 23:04:36 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 20:55:29 +0200 |
wenzelm |
moved IsaPlanner from Provers to Tools;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 14:34:06 +0200 |
wenzelm |
proper loading of ML files;
|
file |
diff |
annotate
|
| Fri, 11 May 2007 00:43:45 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 20 Jan 2007 14:09:27 +0100 |
wenzelm |
tuned ML setup;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2006 23:43:53 +0100 |
wenzelm |
converted legacy ML scripts;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2006 18:07:16 +0100 |
wenzelm |
updated (binder) syntax/notation;
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
| Thu, 01 Jun 2006 21:14:54 +0200 |
wenzelm |
lemmas strip;
|
file |
diff |
annotate
|
| Sat, 20 May 2006 23:36:49 +0200 |
wenzelm |
removed obsolete 'finalconsts';
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:01 +0200 |
wenzelm |
tuned concrete syntax -- abbreviation/const_syntax;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2006 18:51:13 +0200 |
wenzelm |
tuned syntax/abbreviations;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:06 +0200 |
wenzelm |
refined 'abbreviation';
|
file |
diff |
annotate
|
| Wed, 22 Feb 2006 22:18:31 +0100 |
wenzelm |
not_equal: replaced syntax translation by abbreviation;
|
file |
diff |
annotate
|
| Tue, 31 Jan 2006 00:43:14 +0100 |
wenzelm |
declare defn rules;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 19:05:24 +0100 |
wenzelm |
added atomize_iff;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Fri, 30 Dec 2005 16:56:57 +0100 |
wenzelm |
fixed final_consts;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:29:14 +0100 |
wenzelm |
structure ProjectRule;
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 00:58:55 +0200 |
wenzelm |
more finalconsts;
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 00:11:10 +0200 |
nipkow |
renamed rules to iprover
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 16:59:51 +0200 |
wenzelm |
avoid old-style infixes;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Tue, 31 May 2005 11:53:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 22 May 2005 16:51:07 +0200 |
wenzelm |
Simplifier already setup in Pure;
|
file |
diff |
annotate
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
| Tue, 07 Dec 2004 11:31:14 +0100 |
paulson |
proof of subst by S Merz
|
file |
diff |
annotate
|
| Tue, 01 Jun 2004 12:33:50 +0200 |
wenzelm |
removed obsolete sort 'logic';
|
file |
diff |
annotate
|
| Wed, 14 Apr 2004 14:13:05 +0200 |
kleing |
use more symbols in HTML output
|
file |
diff |
annotate
|
| Thu, 16 Oct 2003 10:31:40 +0200 |
paulson |
partial conversion to Isar scripts
|
file |
diff |
annotate
|
| Wed, 15 Jan 2003 16:44:21 +0100 |
paulson |
moving "let" from ZF to FOL
|
file |
diff |
annotate
|
| Wed, 31 Jul 2002 14:34:08 +0200 |
paulson |
new theorem eq_commute
|
file |
diff |
annotate
|
| Mon, 25 Feb 2002 20:48:14 +0100 |
wenzelm |
clarified syntax of ``long'' statements: fixes/assumes/shows;
|
file |
diff |
annotate
|
| Tue, 12 Feb 2002 20:25:58 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 08 Jan 2002 00:03:42 +0100 |
wenzelm |
syntax "_not_equal";
|
file |
diff |
annotate
|
| Wed, 05 Dec 2001 03:00:39 +0100 |
wenzelm |
sym declarations;
|
file |
diff |
annotate
|
| Tue, 04 Dec 2001 02:00:14 +0100 |
wenzelm |
renamed RuleContext to ContextRules;
|
file |
diff |
annotate
|
| Mon, 03 Dec 2001 21:03:06 +0100 |
wenzelm |
setup "rules" method;
|
file |
diff |
annotate
|
| Fri, 09 Nov 2001 00:09:47 +0100 |
wenzelm |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
file |
diff |
annotate
|
| Fri, 02 Nov 2001 22:01:07 +0100 |
wenzelm |
transitive declared in Pure;
|
file |
diff |
annotate
|
| Sun, 28 Oct 2001 21:10:47 +0100 |
wenzelm |
equal_intr_rule already declared in Pure;
|
file |
diff |
annotate
|
| Fri, 26 Oct 2001 23:59:13 +0200 |
wenzelm |
atomize_conj;
|
file |
diff |
annotate
|
| Sat, 20 Oct 2001 20:18:45 +0200 |
wenzelm |
calculational rules moved from FOL to IFOL;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 22:15:07 +0200 |
wenzelm |
moved rulify to ObjectLogic;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 19:59:15 +0200 |
wenzelm |
judgment Trueprop;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2001 12:11:39 +0200 |
wenzelm |
declare impE iffD1 iffD2 ad elim of Pure;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2001 15:28:00 +0200 |
wenzelm |
atomize stuff from theory FOL;
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 20:47:54 +0200 |
wenzelm |
updated setup;
|
file |
diff |
annotate
|
| Fri, 04 Aug 2000 22:55:08 +0200 |
wenzelm |
setup hypsubst_setup;
|
file |
diff |
annotate
|