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 !/?;

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

added asym rule;

tuned print_state;

tuned strings_of_context; fix: check identifier;

pr / no_pr: maintain Toplevel.quiet;

tuned print_state; quiet flag;