Removal of tactical STATE

fixed polymorphic val;

tuned congs: standard;

improved simp tracing;

added simplification meta rules;

tmp fix to accomodate rep_ss changes;

added rewrite_thm;

tuned apsome;

added error_msg;

tuned error / warning;

added print_ss; improved merge;

added dest_mss, merge_mss; fixed matching of simproc lhss;

tuned title;

added dest and merge operations;

added pretty_cterm;

improved print_cs;

Cosmetic changes: margins, indentation, ...

Now possibility_tac is an explicit function, in order to delay the evaluation of \!simpset

Cosmetic changes: margins, indentation, ...

Now possibility_tac and basic_possibility_tac are explicit functions, in order to delay the evaluation of \!simpset

Deleted the superfluous assumption A ~= B, which must hold anyway by induction

Fixed the spelling of AUTH_NAMES--it could not have worked before\!

Option is a synonym for General because MLWorks does not yet provide Option as a separate structure

Removal of the tactical STATE

Removal of the tactical STATE

tuned error propagation msg;

defs may now be conditional; improved output of warnings / errors;

renamed |-> <-| <-> to Parse/PrintRule;

tuned warning;

tuned warnings; print_current_goals_fn, result_error_fn hooks replace print_goals_ref;

considered removal of print_goals_ref;

defs: allow conditions;