Thu, 16 Feb 2006 00:09:46 +0100 |
wenzelm |
tuned subst_bound(s);
|
changeset |
files
|
Wed, 15 Feb 2006 23:57:06 +0100 |
obua |
fixed bugs, added caching
|
changeset |
files
|
Wed, 15 Feb 2006 21:35:13 +0100 |
wenzelm |
added cases_node;
|
changeset |
files
|
Wed, 15 Feb 2006 21:35:12 +0100 |
wenzelm |
replaced qualified_force_prefix to sticky_prefix;
|
changeset |
files
|
Wed, 15 Feb 2006 21:35:11 +0100 |
wenzelm |
removed distinct, renamed gen_distinct to distinct;
|
changeset |
files
|
Wed, 15 Feb 2006 21:35:11 +0100 |
wenzelm |
check_text: Toplevel.node option;
|
changeset |
files
|
Wed, 15 Feb 2006 21:35:09 +0100 |
wenzelm |
init/exit no longer change the theory (no naming);
|
changeset |
files
|
Wed, 15 Feb 2006 21:35:09 +0100 |
wenzelm |
evaluate antiquotes depending on Toplevel.node option;
|
changeset |
files
|
Wed, 15 Feb 2006 21:35:07 +0100 |
wenzelm |
simplified presentation commands;
|
changeset |
files
|
Wed, 15 Feb 2006 21:35:06 +0100 |
wenzelm |
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
|
changeset |
files
|
Wed, 15 Feb 2006 21:35:06 +0100 |
wenzelm |
removed qualified_force_prefix;
|
changeset |
files
|
Wed, 15 Feb 2006 21:35:04 +0100 |
wenzelm |
replaced qualified_force_prefix to sticky_prefix;
|
changeset |
files
|
Wed, 15 Feb 2006 21:35:04 +0100 |
wenzelm |
chop is no longer pervasive;
|
changeset |
files
|
Wed, 15 Feb 2006 21:35:02 +0100 |
wenzelm |
rewrite_cterm: Thm.adjust_maxidx prevents unnecessary increments on rules;
|
changeset |
files
|