Tue, 11 Nov 2014 13:44:09 +0100 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
Tue, 11 Nov 2014 10:54:52 +0100 |
wenzelm |
more Isar proof methods;
|
file |
diff |
annotate
|
Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
Sun, 09 Nov 2014 17:04:14 +0100 |
wenzelm |
proper context for match_tac etc.;
|
file |
diff |
annotate
|
Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
Sat, 16 Aug 2014 11:35:33 +0200 |
wenzelm |
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
|
file |
diff |
annotate
|
Sat, 05 Jul 2014 13:39:53 +0200 |
wenzelm |
modernized definitions;
|
file |
diff |
annotate
|
Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
Sat, 27 Apr 2013 20:50:20 +0200 |
wenzelm |
uniform Proof.context for hyp_subst_tac;
|
file |
diff |
annotate
|
Wed, 23 May 2012 15:57:12 +0200 |
wenzelm |
eliminated obsolete fastsimp;
|
file |
diff |
annotate
|
Thu, 12 Apr 2012 18:39:19 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
Fri, 28 Oct 2011 23:41:16 +0200 |
wenzelm |
tuned Named_Thms: proper binding;
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 18:11:20 +0200 |
wenzelm |
eliminated old List.nth;
|
file |
diff |
annotate
|
Wed, 12 Jan 2011 16:33:04 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
Tue, 17 Aug 2010 19:36:39 +0200 |
haftmann |
more antiquotations
|
file |
diff |
annotate
|
Fri, 23 Apr 2010 23:35:43 +0200 |
wenzelm |
mark schematic statements explicitly;
|
file |
diff |
annotate
|
Thu, 29 Oct 2009 17:58:26 +0100 |
wenzelm |
standardized filter/filter_out;
|
file |
diff |
annotate
|
Thu, 30 Jul 2009 12:20:43 +0200 |
wenzelm |
qualified Subgoal.FOCUS;
|
file |
diff |
annotate
|
Thu, 30 Jul 2009 11:23:57 +0200 |
wenzelm |
FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
|
file |
diff |
annotate
|
Sun, 26 Jul 2009 19:54:37 +0200 |
wenzelm |
tuned eval_tac: eliminated unused METAHYPS (FOCUS fails due to schematic goals);
|
file |
diff |
annotate
|
Thu, 02 Jul 2009 17:34:14 +0200 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
file |
diff |
annotate
|
Fri, 13 Mar 2009 23:50:05 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|
Wed, 31 Dec 2008 00:08:11 +0100 |
wenzelm |
use regular Term.add_vars, Term.add_frees etc.;
|
file |
diff |
annotate
|
Mon, 16 Jun 2008 22:13:39 +0200 |
wenzelm |
pervasive RuleInsts;
|
file |
diff |
annotate
|
Sat, 14 Jun 2008 23:52:51 +0200 |
wenzelm |
proper context for tactics derived from res_inst_tac;
|
file |
diff |
annotate
|
Sat, 14 Jun 2008 23:19:51 +0200 |
wenzelm |
proper context for tactics derived from res_inst_tac;
|
file |
diff |
annotate
|
Wed, 11 Jun 2008 15:40:20 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Tue, 25 Mar 2008 19:39:57 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|