Goals.reset_goals;

reset_goals;

intro+;

remove tmp files;

tuned;

renamed 'single' to 'some_rule'; added 'intro', 'elim';

renamed Cons to Consq in order to avoid clash with List.Cons;

Tuned some comments.

Path for remote theory browsing information is now stored in referece variable rpath.

-m option;

replaced "op #" by "Cons";

'a list: Nil, Cons;

tuned msg;

disable_pr, enable_pr;

deleted obsolete assignment

restored a high precedence to unary minus

inserted Id: lines

new theory Real/Hyperreal/HyperDef and file fuf.ML

forgot to write back adaption of onlysimps

tuned;

tuned;

exchanged finish_tac and unsafe_finish_tac (the more important one) in simpset basic_gen_simp_tac now takes a looper as _explicit_ argument removed superfluous argument of solve_all_tac corrected safe_asm_full_simp_tac: now also with mutual simplification of prems

re-added refl in safe_solver

removed warn_theory_style;

fixed thy_only;

tuned prompts;

isamode;

user infaces: tuned, added ProofGeneral;

bib;

-m option;

Tuned.

Removed * reset HOL_quantifiers by default, i.e. quantifiers are printed as ALL/EX rather than !/?;