| Sat, 17 Jun 2006 19:37:45 +0200 |
wenzelm |
RuleCases.mutual_rule: ctxt;
|
file |
diff |
annotate
|
| Mon, 12 Jun 2006 21:19:00 +0200 |
wenzelm |
tuned Seq/Envir/Unify interfaces;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Wed, 22 Feb 2006 22:18:32 +0100 |
wenzelm |
simplified Pure conjunction;
|
file |
diff |
annotate
|
| Fri, 10 Feb 2006 02:22:16 +0100 |
wenzelm |
Args/Attrib syntax: Context.generic;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:59:00 +0100 |
wenzelm |
Logic.rlist_abs;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2006 17:28:52 +0100 |
wenzelm |
LocalDefs.add_def;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 19:03:02 +0100 |
wenzelm |
moved theorem tags from Drule to PureThy;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
| Tue, 10 Jan 2006 19:33:30 +0100 |
wenzelm |
fix_tac: no warning;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2006 12:26:25 +0100 |
wenzelm |
RuleCases.make_common/nested;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2006 17:14:07 +0100 |
wenzelm |
RuleCases.strict_mutual_rule;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 18:36:27 +0100 |
wenzelm |
removed obsolete atomize_old;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 15:16:44 +0100 |
wenzelm |
proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:28:51 +0100 |
wenzelm |
simplified setup: removed dest_concls, local_impI, conjI;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2005 08:06:59 +0100 |
haftmann |
introduced new map2, fold
|
file |
diff |
annotate
|
| Tue, 29 Nov 2005 23:00:20 +0100 |
wenzelm |
moved nth_list to Pure/library.ML;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2005 20:57:51 +0100 |
wenzelm |
induct: insert defs in object-logic form;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2005 18:58:36 +0100 |
wenzelm |
fix_tac: proper treatment of major premises in goal;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2005 22:23:52 +0100 |
wenzelm |
more robust revert_skolem;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2005 18:52:02 +0100 |
wenzelm |
(co)induct: taking;
|
file |
diff |
annotate
|
| Tue, 22 Nov 2005 19:34:43 +0100 |
wenzelm |
make coinduct actually work;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2005 14:21:02 +0100 |
wenzelm |
induct: CONJUNCTS for multiple goals;
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 17:45:24 +0100 |
wenzelm |
induct: support local definitions to be passed through the induction;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2005 20:57:17 +0100 |
wenzelm |
induct method: fixes;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 22:27:47 +0200 |
wenzelm |
accomodate simplified Thm.lift_rule;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:41 +0200 |
wenzelm |
Goal.norm_hhf_rule, Goal.init;
|
file |
diff |
annotate
|
| Tue, 14 Jun 2005 21:56:57 +0200 |
wenzelm |
export cases_tac, induct_tac;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 18:57:18 +0200 |
berghofe |
Adapted to new interface of instantiation and unification / matching functions.
|
file |
diff |
annotate
|