Eliminated some infixes.

Eliminated some infixes.

Renamed sum_case to basic_sum_case and removed translations for sum_case to avoid conflicts with the constant sum_case introduced in Datatype.thy.

tuned;

replaced 'ProofGeneral' by 'Proof General';

Modified section about generation of theory browsing information. Documented new -P option.

new version from Konrad with "lazy" (deferred) definitons

tidied some proofs

new primitive rule permute_prems to underlie defer_tac and rotate_prems

freeze_thaw does nothing if no variables

Added take_all and drop_all to simpset.

eliminated HOL_quantifiers (replaced by "HOL" print mode);

may_load_file; use_thy etc.: warn_finished; added begin_update_theory; added quiet_update_thy;

ThyInfo.may_load_file;

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;

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;