1999-08-17 wenzelm 1999-08-17 tuned;
1999-08-17 wenzelm 1999-08-17 renamed 'single' to 'some_rule'; added 'intro', 'elim';
1999-08-17 wenzelm 1999-08-17 renamed Cons to Consq in order to avoid clash with List.Cons;
1999-08-17 berghofe 1999-08-17 Tuned some comments.
1999-08-17 berghofe 1999-08-17 Path for remote theory browsing information is now stored in referece variable rpath.
1999-08-17 wenzelm 1999-08-17 -m option;
1999-08-16 wenzelm 1999-08-16 replaced "op #" by "Cons";
1999-08-16 wenzelm 1999-08-16 'a list: Nil, Cons;
1999-08-16 wenzelm 1999-08-16 tuned msg;
1999-08-16 wenzelm 1999-08-16 disable_pr, enable_pr;
1999-08-16 paulson 1999-08-16 deleted obsolete assignment
1999-08-16 paulson 1999-08-16 restored a high precedence to unary minus
1999-08-16 paulson 1999-08-16 inserted Id: lines
1999-08-16 paulson 1999-08-16 new theory Real/Hyperreal/HyperDef and file fuf.ML
1999-08-16 oheimb 1999-08-16 forgot to write back adaption of onlysimps
1999-08-16 wenzelm 1999-08-16 tuned;
1999-08-16 wenzelm 1999-08-16 tuned;
1999-08-16 oheimb 1999-08-16 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
1999-08-16 oheimb 1999-08-16 re-added refl in safe_solver
1999-08-16 wenzelm 1999-08-16 removed warn_theory_style;
1999-08-16 wenzelm 1999-08-16 fixed thy_only;
1999-08-16 wenzelm 1999-08-16 tuned prompts;
1999-08-16 wenzelm 1999-08-16 isamode;
1999-08-16 wenzelm 1999-08-16 user infaces: tuned, added ProofGeneral;
1999-08-16 wenzelm 1999-08-16 bib;
1999-08-16 wenzelm 1999-08-16 -m option;
1999-08-12 berghofe 1999-08-12 Tuned.
1999-08-11 nipkow 1999-08-11 Removed * reset HOL_quantifiers by default, i.e. quantifiers are printed as ALL/EX rather than !/?;
1999-08-11 nipkow 1999-08-11 * set HOL_quantifiers by default, i.e. quantifiers are printed as !/? rather than ALL/EX;
1999-08-09 wenzelm 1999-08-09 added asym rule;
1999-08-09 wenzelm 1999-08-09 tuned print_state;
1999-08-09 wenzelm 1999-08-09 tuned strings_of_context; fix: check identifier;
1999-08-09 wenzelm 1999-08-09 pr / no_pr: maintain Toplevel.quiet;
1999-08-09 wenzelm 1999-08-09 tuned print_state; quiet flag;
1999-08-09 wenzelm 1999-08-09 append user rules;
1999-08-09 wenzelm 1999-08-09 theory loader actions;
1999-08-06 wenzelm 1999-08-06 made SML happy;
1999-08-06 wenzelm 1999-08-06 tuned;
1999-08-06 wenzelm 1999-08-06 proper ProofGeneral/isa setup;
1999-08-06 wenzelm 1999-08-06 simplified ML handling;
1999-08-06 wenzelm 1999-08-06 added pretend_use; simplified ML handling; loaded_files: include thy; perform Remove *before* actual deletion; perform: made bullet proof;
1999-08-06 wenzelm 1999-08-06 simplified handling of ML file; improved master info;
1999-08-06 paulson 1999-08-06 the whole file is now loaded only if SVC is enabled
1999-08-06 paulson 1999-08-06 re-organization of theorems from Alloc and PPROD, partly into new theory Lift_prog
1999-08-06 paulson 1999-08-06 svc_enabled is now declared as a function
1999-08-06 paulson 1999-08-06 new theory UNITY/Lift_prog
1999-08-06 wenzelm 1999-08-06 External reasoning tools;
1999-08-06 paulson 1999-08-06 no longer gives a default value to SVC_MACHINE
1999-08-06 paulson 1999-08-06 extra comment
1999-08-06 paulson 1999-08-06 now catches exn THEORY and prints an error message
1999-08-06 paulson 1999-08-06 some hard propositional examples
1999-08-06 paulson 1999-08-06 new theory ex/svc_test.thy
1999-08-05 wenzelm 1999-08-05 removed obsolete addsimps update_defs;
1999-08-05 wenzelm 1999-08-05 record_simproc for sel-upd (by Sebastian Nanz); removed record_splitter by default;
1999-08-05 wenzelm 1999-08-05 change_simpset_of;
1999-08-05 wenzelm 1999-08-05 local goals: after_qed;
1999-08-04 wenzelm 1999-08-04 tuned;
1999-08-04 wenzelm 1999-08-04 added isabelle-sys, proofgeneral;
1999-08-04 wenzelm 1999-08-04 improved \NOTE; added \BYY;
1999-08-03 wenzelm 1999-08-03 tuned; added sect, subsect, subsubsect;