made the perm_simp tactic to understand options such as (no_asm)

type thm: fully internal derivation, no longer exported; incorporate former deriv.ML as internal abstract type; added rudimentary promise interface; tuned; added is_named (does not require finished derivation);

added is_finished;

added Promise constructor, which is similar to Oracle but may be replaced later; added promise_proof; export min_proof, mk_min_proof; moved infer_derivs to thm.ML as derive_rule0/1/2; tuned oracles_of_proof; added is_named;

removed deriv.ML which is now incorporated into thm.ML;

added reject_draft;

type thm: fully internal derivation, no longer exported;

generic quickcheck framework

TEMPORARY: make batch run happy

absolute Library path

different session branches for HOL-Plain vs. Plain

temporary workaround for class constants

corrected sort intersection

some steps towards generic quickcheck framework

fixed headers

added some fragments from website

made SML/NJ happy;

Isar toplevel editor model.

future tasks: support boolean priorities (true = high, false = low/irrelevant);

output_sync is now public;

added props_text (from isar_syn.ML);

moved Isar editor commands from isar_syn.ML to isar.ML; P.props_text;

moved Isar editor commands from isar_syn.ML to isar.ML;

added Isar/isar.scala;

avoid using implicit assumptions

add theory graph to ZF document

made SMLNJ happy

jar: include sources;

tuned;

eval_term: CRITICAL due to eval_result; simplified oracle interface;