print_state hook, obeys Goals.current_goals_markers by default;

print_state: use begin_goal from Goals.current_goals_markers;

added undos, redos;

tty: issue wakeup;

std_output, prefix_lines;

better miniscoping rules: the premise C~={} is not good because Safe_tac eliminates such assumptions.

fixed method syntax;

break: exhibit state stack;

match_bind: 'as' patterns; statements: 'is' patterns;

let: 'as' patterns; statements: propp ('is' patterns);

match_bind(_i): 'as' patterns; assume, theorem, show etc.: propp; tuned qed msg;

term_pat vs. prop_pat; added bind_propp(_i); assume: propp;

term_pat vs. prop_pat;

no warning for "it" theorems;

tidied

Finally removing "Compl" from HOL

exn_message FAIL;

blast: cla_method';

export simp_modifiers;

expoer cla_method('), cla_modifiers;

method setup;

tuned comments;

'prop', 'term', 'typ';

load;

export exn_message;

removed trace;

BREAK: include state; report Attrib.ATTRIB_FAIL, Method.METHOD_FAIL;

have_tthms; assume: store actual asms;