added use_thy_only;

added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;

avoid string constants;

qed indexed.

typedef_proof: pass interactive flag;

tuned; added prompt_state_fn hook; added kill operation; provide toplevel node history, nests with proof history; toplevel prompt includes nest level; more robust recovery from stale signatures;

cleaned comments; global statements: init history according to interactive mode; local qed: pass interactive mode; init theory: kill operation;

renamed 'begin' / 'end' to '{{' / '}}'; added 'kill'; rename 'type' to 'typ';

history commands;

tuned;