begin_update_theory;

PASS(_MODE): works better without space (why?);

removed HOL_quantifiers;

HOL_quantifiers;

replaced HOL_quantifiers flag by "HOL" print mode; simplified HOL basic syntax (more orthogonal);

turned SVC_Oracle into a new-style theory in order to get automatic handling of its additional dependency on Tools/svc_funcs.ML;

Better handling of path for remote theory browsing information.

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;