removed ad-hoc atp_hook, cal_atp; removed depth_of; tuned;

Toplevel.actual_proof;

avoid excessive exceptions;

Graph: fast_string_ord;

export eq_brl;

added subtract; improved interface; tuned;

export eq_rrule; improved Net interface;

removed obsolete delta stuff;

open ReconPrelim Recon_Transfer;

open ReconPrelim ReconTranslateProof; removed second copy of exception ASSERTION;

tuned;

use Toplevel.print_state_hook instead of adhoc Proof.atp_hook; added call_atp: bool ref; do 'setmp print_mode []', which is more robust than manual ref manipulation; added subtract_simpset, subtract_claset (supercede delta approximation);

tuned concat_with_and; improved Net interface;

improved Net interface;

* Isar session: The initial use of ROOT.ML is now always timed;

Add acceptedpgipelems message

auto update

generlization of some "nat" theorems

relevance filtering is now optional

tidied

fixed comment-out;

fix

Add management for current working directory

(fix for an accidental commit)

Note about theorem dependencies including themselves.

Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc

(intermediate commit)

(corrected wrong commit)

(intermediate commit)

- added cplex package to HOL/Matrix