Assumption.assume;

moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);

removed obsolete equal_abs_elim(_list);

removed obsolete pretty_thm_no_quote;

added Pure/assumption.ML;

moved basic assumption operations from structure ProofContext to Assumption;

tuned proofs;

Local assumptions, parameterized by export rules.

updated;

import(T): result includes fixed types/terms; focus: tuned interface;

focus: result record includes (fixed) schematic variables; SUBGOAL: disallow pending subgoals, more robust re-composition;

Variable.import(T): result includes fixed types/terms;

linear arithmetic splits certain operators (e.g. min, max, abs)

added eval_term

updated;

fixed LaTeX problem;

added eval_term

Removed wrong sentence (Simon Funke)

moved pprint functions to Isar/proof_display.ML;

Tactical operations depending on local subgoal structure.

moved pprint functions to Isar/proof_display.ML; added primitive add_assumes; tuned internal prems: no names;

export goal_tac (was internal refine_tac);

added Pure/subgoal.ML;

updated;

raw symbols: disallow dot to avoid confusion in NameSpace.unpack;

avoid Term.is_funtype;

avoid structure Char;

added variant_abs (from term.ML); tuned;

added find_free (from term.ML);

added is/to_ascii_lower/upper; tuned alphanum -- needs more work;