| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Wed, 29 May 2013 18:25:11 +0200 |
wenzelm |
tuned signature -- more explicit flags for low-level Thm.bicompose;
|
file |
diff |
annotate
|
| Sat, 13 Oct 2012 16:19:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 21:50:04 +0200 |
wenzelm |
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 11 Dec 2009 20:43:41 +0100 |
wenzelm |
Subgoal.FOCUS etc.: resulting goal state is normalized as usual for resolution;
|
file |
diff |
annotate
|
| Wed, 05 Aug 2009 15:39:34 +0200 |
wenzelm |
SUBPROOF: recovered Goal.check_finished;
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 17:54:57 +0200 |
wenzelm |
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 12:20:43 +0200 |
wenzelm |
qualified Subgoal.FOCUS;
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 11:23:17 +0200 |
wenzelm |
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2009 20:57:19 +0200 |
wenzelm |
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2009 19:38:02 +0200 |
wenzelm |
retrofit: actually handle schematic variables -- need to export into original context;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2009 13:12:54 +0200 |
wenzelm |
advanced retrofit, which allows new subgoals and variables;
|
file |
diff |
annotate
|
| Wed, 24 Jun 2009 21:28:02 +0200 |
wenzelm |
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 23:36:55 +0100 |
wenzelm |
provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2007 19:24:13 +0200 |
wenzelm |
renamed Variable.import to import_thms (avoid clash with Alice keywords);
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:29 +0100 |
wenzelm |
qualified MetaSimplifier.norm_hhf(_protect);
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 19:39:07 +0200 |
wenzelm |
Thm.dest_arg;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:55 +0200 |
wenzelm |
Variable.focus_subgoal;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:09 +0200 |
wenzelm |
tuned interfaces;
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:37:42 +0200 |
wenzelm |
focus: result record includes (fixed) schematic variables;
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 00:44:48 +0200 |
wenzelm |
Tactical operations depending on local subgoal structure.
|
file |
diff |
annotate
|