| Tue, 03 Jul 2007 17:49:55 +0200 |
chaieb |
reflection and reification methods now manage Context data
|
changeset |
files
|
| Tue, 03 Jul 2007 17:49:53 +0200 |
chaieb |
Context Data for the reflection and reification methods
|
changeset |
files
|
| Tue, 03 Jul 2007 17:28:36 +0200 |
huffman |
rename class dom to ring_1_no_zero_divisors
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:17 +0200 |
wenzelm |
rewrite_goal_tac;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:16 +0200 |
wenzelm |
replaced Conv.goals_conv by Conv.prems_conv;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:15 +0200 |
wenzelm |
exported meta_rewrite_conv;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:15 +0200 |
wenzelm |
CONVERSION tactical;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:13 +0200 |
wenzelm |
removed obsolete eta_long_tac;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:13 +0200 |
wenzelm |
added CONVERSION tactical;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:11 +0200 |
wenzelm |
tuned rotate_prems;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:11 +0200 |
wenzelm |
moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:09 +0200 |
wenzelm |
removed obsolete mk_conjunction_list, intr/elim_list;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:09 +0200 |
wenzelm |
removed obsolete goals_conv (cf. prems_conv);
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:07 +0200 |
wenzelm |
Conjunction.intr/elim_balanced;
|
changeset |
files
|