init_empty: invoke operation *after* safe_exit;

added simultaneous use_thys; deps: removed obsolete present'' flag;

avoid polymorphic equality;

blast_hyp_subst_tac: plain bool argument;

Context data for QE in DLO (Langford's algorithm)

Quantifier elimination for Dense linear orders after Langford

Tuned proof : dlo replaced by ferrack

tuned

Renamed attribute dlo into attribute ferrack

Added quantifier elimination in dense linear orders after Langford; locale dense_linear_order renamed to constr_dense_linear_order (since it requires the beween constant). locale dense_linear_order is now the classical definition of DLO. constr_dense_linear_order is an instance of dense_linear_order; Method dlo now applies the langford QE, odl Method dlo renamed to ferrack, since it ia a QE only in interpretations where between is interpreted in a manner to vanish after substitution.

Tunes Proof

begin_theory: simplified interface, keep thy info empty until end_theory;

clarified init/begin_theory: no longer depend on thy_info.ML; tuned;

clarified Present.init;

simplified ThyInfo.begin_theory;

load present.ML earlier: no longer depend on thy_info.ML;

chmod u+rw on all files;

tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);

deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy); begin_theory: quiet_update_thys in interactive mode, removed no weak_use_thy in batch mode; misc tuning;

tuned;

dropped Nat legacy bindings

check_file: fall back on Path.current;

tuned;

* Theory loader: be more serious about observing the static theory header specifications; * Theory loader: optional support for content-based file identification;