2001-11-28 ago print_state: up to 7 result names;
2001-11-19 ago improved treatment of common result name;
2001-11-19 ago multi_theorem: common statement header (covers *all* results);
2001-11-16 ago finish_global: Drule.strip_shyps_warning (just for warning);
2001-11-12 ago empty rule_context for multiple goals;
2001-11-11 ago added multi_theorem(_i);
2001-11-07 ago locale_prefix: Sign.base_name;
2001-11-06 ago pretty_goals_local: observes context syntax;
2001-11-06 ago theorem(_i): locale atts;
2001-11-05 ago pretty/print functions with context;
2001-11-04 ago theorem(_i): locale elements;
2001-11-01 ago theorem: locale argument;
2001-10-31 ago theorem(_i): locale argument;
2001-10-31 ago Removed name_thm from finish_global.
2001-10-31 ago finish_global: Tactic.norm_hhf;
2001-10-30 ago tuned;
2001-10-24 ago simplified ProofContext.assume interface;
2001-10-23 ago moved RANGE to tctical.ML;
2001-10-23 ago removed export_thm;
2001-10-22 ago moved local defs to proof.ML (for locales);
2001-10-16 ago simplified exporter interface;
2001-10-16 ago support impromptu terminology of cases parameters;
2001-10-13 ago generic theorem kinds;
2001-09-08 ago print_state: subgoals;
2001-09-04 ago renamed "antecedent" case to "rule_context";
2001-08-31 ago Tuned naming of theorems.
2001-02-07 ago val get_goal: state -> context * (thm list * thm);
2001-01-18 ago made SML/XL happy;
2001-01-18 ago show(_i): check goal;
2001-01-09 ago avoid renaming of params in cases;
2001-01-06 ago moved norm_hhf_tac to Pure/tactic.ML;
2000-11-30 ago removed get_goal;
2000-11-21 ago tag result with name reference to final binding (basically just a comment);
2000-11-13 ago tuned statement args;
2000-11-10 ago norm_hhf_tac;
2000-11-06 ago RuleCases.make true;
2000-11-03 ago tuned names;
2000-10-30 ago tuned goals output;
2000-10-30 ago Added antiquotation "subgoals".
2000-10-24 ago added pretty_goals;
2000-08-01 ago tuned;
2000-07-30 ago export RANGE, hard_asm_tac, soft_asm_tac;
2000-07-13 ago invoke_case: bind_skolem;
2000-06-29 ago facts: handle multiple lists of arguments;
2000-05-28 ago case 'antecedent';
2000-05-05 ago GPLed;
2000-04-17 ago tuned msg;
2000-04-15 ago next_block: reset_facts;
2000-04-05 ago tuned comment;
2000-03-30 ago support Hindley-Milner polymorphisms in binds and facts;
2000-03-26 ago tuned output;
2000-03-23 ago tuned output;
2000-03-21 ago soft_asm_tac: hack to norm goal;
2000-03-17 ago next_block: allow in non-goal blocks as well (experimental);
2000-03-15 ago pretty chunks;
2000-03-14 ago invoke_case: include attributes;
2000-03-08 ago invoke_case: name assumption;
2000-03-08 ago generalized FINDGOAL, HEADGOAL;
2000-02-14 ago tuned msg;
2000-02-13 ago refine_end;