| Fri, 21 Oct 2005 18:14:50 +0200 | wenzelm | Goal.conclude; | changeset | files |
| Fri, 21 Oct 2005 18:14:49 +0200 | wenzelm | moved SELECT_GOAL to goal.ML; | changeset | files |
| Fri, 21 Oct 2005 18:14:48 +0200 | wenzelm | moved norm_hhf_rule, prove etc. to goal.ML; | changeset | files |
| Fri, 21 Oct 2005 18:14:47 +0200 | wenzelm | added simplification tactics and rules (from meta_simplifier.ML); | changeset | files |
| Fri, 21 Oct 2005 18:14:46 +0200 | wenzelm | moved various simplification tactics and rules to simplifier.ML; | changeset | files |
| Fri, 21 Oct 2005 18:14:45 +0200 | wenzelm | warn_obsolete for goal commands -- danger of disrupting a local proof context; | changeset | files |