wenzelm [Fri, 21 Oct 2005 18:14:52 +0200] rev 17972
do not export find_thms;
wenzelm [Fri, 21 Oct 2005 18:14:51 +0200] rev 17971
use obsolete goals.ML here;
wenzelm [Fri, 21 Oct 2005 18:14:50 +0200] rev 17970
Goal.conclude;
wenzelm [Fri, 21 Oct 2005 18:14:49 +0200] rev 17969
moved SELECT_GOAL to goal.ML;
wenzelm [Fri, 21 Oct 2005 18:14:48 +0200] rev 17968
moved norm_hhf_rule, prove etc. to goal.ML;
moved asm_rewrite_goal_tac to simplifier.ML;
wenzelm [Fri, 21 Oct 2005 18:14:47 +0200] rev 17967
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm [Fri, 21 Oct 2005 18:14:46 +0200] rev 17966
moved various simplification tactics and rules to simplifier.ML;
wenzelm [Fri, 21 Oct 2005 18:14:45 +0200] rev 17965
warn_obsolete for goal commands -- danger of disrupting a local proof context;
Goal.init, Goal.conclude, Goal.norm_hhf_rule;
shortcuts no longer pervasive (cf. structure OldGoals);
wenzelm [Fri, 21 Oct 2005 18:14:44 +0200] rev 17964
renamed triv_goal to goalI, rev_triv_goal to goalD;
removed mk_triv_goal (cf. Goal.init);
wenzelm [Fri, 21 Oct 2005 18:14:43 +0200] rev 17963
added goal.ML;
moved use of goals.ML;