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;

begin_theory: Theory.checkpoint for immediate uses ensures that ML evaluation always starts with non-draft @{theory};

updated generated file;

simplified oracle interface;

show: non-critical testing;

added deriv.ML: Abstract derivations based on raw proof terms.

termination prover for "fun" can be configured using context data.

updated generated file;

unchecked $ISABELLE_HOME_USER/etc/settings;

use_text/use_file now depend on explicit ML name space;

threads work only for Poly/ML 5.2 or later; global ML bindings are now thread-safe;

* ML bindings produced via Isar commands are stored within the Isar context. * Command 'ML_prf' is analogous to 'ML' but works within a proof context.

added ML_prf;

updated generated file;

added inherit_env;

added map_contexts;

ML_prf: inherit env for all contexts within the proof;

shutdown only if Multithreading.available;

ML_Context.evaluate: proper context (for ML environment); use_text/use_file now depend on explicit ML name space;

ML_Context.evaluate: proper context (for ML environment);

simplified ML_Context.eval_in -- expect immutable Proof.context value;

proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);

simplified ML_Context.eval_in -- expect immutable Proof.context value; parse_code: operate on thy, which contains the ML environment;