| 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 |
| Fri, 21 Oct 2005 18:14:44 +0200 | wenzelm | renamed triv_goal to goalI, rev_triv_goal to goalD; | changeset | files |
| Fri, 21 Oct 2005 18:14:43 +0200 | wenzelm | added goal.ML; | changeset | files |
| Fri, 21 Oct 2005 18:14:42 +0200 | wenzelm | added goal.ML; | changeset | files |
| Fri, 21 Oct 2005 18:14:41 +0200 | wenzelm | Goal.norm_hhf_rule, Goal.init; | changeset | files |