more careful evaluation of ML text, prevents spurious output;

date: forcing LC_ALL=C prevents funny file names;

root function: restore default interrupt handler; output file: avoid .exe (e.g. for Cygwin);

patched up the proofs agsin

removed use of put_name_hint, as the ATP linkup no longer needs this

reorganized structure Tactic vs. MetaSimplifier;

begin/end blocks; tuned notation;

abbrevs: more careful interpretation, avoid dynamic references to local names;

definition/abbreviation: single argument;

simplified add_abbrev -- single argument;

removed obsolete references to ProofGeneral/isa;

added input_mode;

tuned print_locale output; add_decls: Thm.internalK;

moved notation/abbrevs to TermSyntax;

expand_term: based on Envir.expand_term; tuned;

thms etc.: proper treatment of internal_fact with selection;

tuned pretty_src output;

simplified add_abbrevs: no mixfix;

added expand_term;

tuned;

Common term syntax declarations.

added Isar/term_syntax.ML;

TermSyntax.notation/abbrevs;

Removal of theorem tagging, which the ATP linkup no longer requires. Suffixes no longer blacklisted.

Removal of theorem tagging, which the ATP linkup no longer requires,

Poly/ML 5.0 setup for Isabelle2005.

reorganized structure Goal vs. Tactic;

export: added explicit term operation;