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 {};