| Mon, 16 Mar 2009 18:24:30 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| 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, 15 Aug 2008 15:50:44 +0200 |
wenzelm |
Args.name_source(_position) for proper position information;
|
file |
diff |
annotate
|
| Wed, 13 Aug 2008 20:57:18 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 22:13:39 +0200 |
wenzelm |
pervasive RuleInsts;
|
file |
diff |
annotate
|
| Sat, 14 Jun 2008 23:20:02 +0200 |
wenzelm |
removed unused excluded_middle_tac;
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 16:43:01 +0200 |
wenzelm |
eliminated obsolete case_split_thm -- use case_split;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 22:55:49 +0100 |
wenzelm |
purely functional setup of claset/simpset/clasimpset;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2008 22:40:01 +0100 |
wenzelm |
pass imp_elim, swap to classical prover;
|
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, 31 May 2007 14:34:05 +0200 |
wenzelm |
tuned header;
|
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
|
| Thu, 27 Jul 2006 13:43:00 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2006 17:28:50 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 06 Jan 2006 18:18:13 +0100 |
wenzelm |
simplified EqSubst setup;
|
file |
diff |
annotate
|
| Fri, 06 Jan 2006 15:18:20 +0100 |
wenzelm |
tuned EqSubst setup;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2005 21:49:39 +0100 |
wenzelm |
removed obsolete cla_dist_concl;
|
file |
diff |
annotate
|
| Fri, 30 Dec 2005 16:56:56 +0100 |
wenzelm |
provide cla_dist_concl;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 18:36:26 +0100 |
wenzelm |
removed obsolete induct_atomize_old;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:28:34 +0100 |
wenzelm |
updated auxiliary facts for induct method;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
| Thu, 08 Jul 2004 19:32:46 +0200 |
wenzelm |
removed obsolete dependency;
|
file |
diff |
annotate
|
| Wed, 20 Aug 2003 11:04:17 +0200 |
paulson |
new case_tac method
|
file |
diff |
annotate
|
| Tue, 01 Jul 2003 10:50:26 +0200 |
paulson |
moved some lemmas here from ZF
|
file |
diff |
annotate
|
| Fri, 30 Aug 2002 16:42:45 +0200 |
paulson |
removal of blast.overloaded
|
file |
diff |
annotate
|
| Wed, 05 Dec 2001 02:59:49 +0100 |
wenzelm |
removed declaration of disjI1, disjI2 (already done in IFOL);
|
file |
diff |
annotate
|
| Wed, 28 Nov 2001 00:37:08 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 19 Nov 2001 20:46:05 +0100 |
wenzelm |
induct method: localize rews for rule;
|
file |
diff |
annotate
|
| Mon, 12 Nov 2001 23:26:18 +0100 |
wenzelm |
induct_atomize: include atomize_conj (for mutual induction);
|
file |
diff |
annotate
|
| Mon, 12 Nov 2001 20:22:23 +0100 |
wenzelm |
val local_imp_def = thm "induct_implies_def";
|
file |
diff |
annotate
|
| Fri, 09 Nov 2001 22:50:32 +0100 |
wenzelm |
theorems case_split = case_split_thm [case_names True False, cases type: o];
|
file |
diff |
annotate
|
| Wed, 31 Oct 2001 01:19:58 +0100 |
wenzelm |
induct_impliesI;
|
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
|
| Thu, 04 Oct 2001 15:28:26 +0200 |
wenzelm |
moved atomize stuff to theory IFOL;
|
file |
diff |
annotate
|
| Sun, 11 Feb 2001 16:31:54 +0100 |
wenzelm |
tuned trans rules;
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 19:00:51 +0100 |
wenzelm |
added atomize_eq;
|
file |
diff |
annotate
|
| Fri, 03 Nov 2000 21:31:11 +0100 |
wenzelm |
"atomize" for classical tactics;
|
file |
diff |
annotate
|
| Mon, 02 Oct 2000 15:13:32 +0200 |
wenzelm |
added == transitive rule (bad idea??);
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 20:47:34 +0200 |
wenzelm |
setup Rulify.setup;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2000 00:55:31 +0200 |
wenzelm |
cong setup now part of Simplifier;
|
file |
diff |
annotate
|
| Fri, 04 Aug 2000 22:54:49 +0200 |
wenzelm |
lemmas atomize = all_eq imp_eq;
|
file |
diff |
annotate
|
| Tue, 01 Aug 2000 11:58:14 +0200 |
wenzelm |
improved comments;
|
file |
diff |
annotate
|
| Fri, 31 Mar 2000 22:22:23 +0200 |
wenzelm |
added cong atts;
|
file |
diff |
annotate
|
| Wed, 15 Mar 2000 18:42:13 +0100 |
wenzelm |
splitter setup;
|
file |
diff |
annotate
|
| Wed, 25 Aug 1999 20:45:19 +0200 |
wenzelm |
proper bootstrap of IFOL/FOL theories and packages;
|
file |
diff |
annotate
|
| Mon, 16 Nov 1998 11:11:42 +0100 |
wenzelm |
attrib_setup;
|
file |
diff |
annotate
|
| Wed, 29 Apr 1998 11:29:39 +0200 |
wenzelm |
tuned setup;
|
file |
diff |
annotate
|
| Sat, 04 Apr 1998 12:28:39 +0200 |
wenzelm |
replaced thy_data by thy_setup;
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:26:58 +0100 |
wenzelm |
added claset thy_data;
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|