avoid OldGoals shortcuts;

* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running. * Internal goals: structure Goal.

Internal goals.

renamed triv_goal to goalI, rev_triv_goal to goalD;

tuned header;

Goal.norm_hhf_rule;

export add_binds_i; invoke_case: AutoBind.no_facts; Goal.init, Goal.conclude;

load_file: setmp OldGoals.legacy true;

improved check_result; Goal.init, Goal.conclude;

Goal.prove_plain;

do not export find_thms;

use obsolete goals.ML here;

Goal.conclude;

moved SELECT_GOAL to goal.ML;

moved norm_hhf_rule, prove etc. to goal.ML; moved asm_rewrite_goal_tac to simplifier.ML;

added simplification tactics and rules (from meta_simplifier.ML);

moved various simplification tactics and rules to simplifier.ML;

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);

renamed triv_goal to goalI, rev_triv_goal to goalD; removed mk_triv_goal (cf. Goal.init);

added goal.ML; moved use of goals.ML;

added goal.ML;

Goal.norm_hhf_rule, Goal.init;

avoid triv_goal and home-grown meta_allE;

OldGoals;