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;

tuned strings_of_context; fix: check identifier;

pr / no_pr: maintain Toplevel.quiet;

tuned print_state; quiet flag;

append user rules;

theory loader actions;

made SML happy;

tuned;

proper ProofGeneral/isa setup;

simplified ML handling;

added pretend_use; simplified ML handling; loaded_files: include thy; perform Remove *before* actual deletion; perform: made bullet proof;

simplified handling of ML file; improved master info;

the whole file is now loaded only if SVC is enabled

re-organization of theorems from Alloc and PPROD, partly into new theory Lift_prog

svc_enabled is now declared as a function

new theory UNITY/Lift_prog

External reasoning tools;

no longer gives a default value to SVC_MACHINE

extra comment

now catches exn THEORY and prints an error message

some hard propositional examples

new theory ex/svc_test.thy

removed obsolete addsimps update_defs;

record_simproc for sel-upd (by Sebastian Nanz); removed record_splitter by default;

change_simpset_of;

local goals: after_qed;

tuned;

added isabelle-sys, proofgeneral;

improved \NOTE; added \BYY;

tuned; added sect, subsect, subsubsect;

improved interest;

tuned;

tuned attdx, methdx; added descr env;

fixed {};

tuned; much more material;

Sara Kalvala: moving the <<...>> notation from LK to Sequents

new examples file for SVC

biconditionals and the natural numbers

added realT

biconditionals and the natural numbers

new examples file for SVC

new chapter on Sequents

\underscoreoff needed because of \underscoreon in previous file

new variables for SVC

SVC

fixed Blast_Data;

blast method: optional depth argument;

export cla_meth(');

tuned;

tuned outer syntax;

handle LIST _;

cat_lines;

provide String structure;

removed obsolete concat;

String.isPrefix

long-overdue updating

new files for the SVC link-up

the SVC oracle theory

the SVC link-up

new files for the SVC link-up

even more stuff;

oracle: '=';

added \text;

Isabelle/Isar macros;

hacking the rail package;

added update_thy_only; moved update_thy;

more;

more stuff;

renamed 'same' to '-';

eliminated METHOD0 in favour of same_tac;

'arith' proof method;

added erule; renamed same to -;

export sysify_path;

split_diff and remove_diff_ss

added parentheses to cope with a possible reduction of the precedence of unary minus

ML_HOME=$ISABELLE_HOME/../smlnj/bin;

HOL-Real target now builds an actual image;

added pretty_setmargin;

congruence rule for |-, etc.

renamed ...thm_pack... to ...pack...

removed the unused SeqVar option

sequents require higher bounds