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;
wenzelm [Fri, 21 Oct 2005 18:14:42 +0200] rev 17962
added goal.ML;
wenzelm [Fri, 21 Oct 2005 18:14:41 +0200] rev 17961
Goal.norm_hhf_rule, Goal.init;
wenzelm [Fri, 21 Oct 2005 18:14:40 +0200] rev 17960
avoid triv_goal and home-grown meta_allE;
wenzelm [Fri, 21 Oct 2005 18:14:38 +0200] rev 17959
OldGoals;