marked some CRITICAL sections; eliminated transform_failure (to avoid critical section for main transactions); removed unused exceptions MetaSimplifier.SIMPROC_FAIL, Attrib.ATTRIB_FAIL, Method.METHOD_FAIL, Antiquote.ANTIQUOTE_FAIL;

marked some CRITICAL sections;

depth flag: plain bool ref; eliminated transform_failure (to avoid critical section for main transactions);

eliminated transform_failure (to avoid critical section for main transactions);

setmp_noncritical (assumes outermost control);

PrintMode.with_modes;

added with_modes, with_default;

marked some CRITICAL sections;

added setmp_noncritical; setmp: CRITICAL;

PrintMode.with_default;

added nbe implementation heading for dictionaries

Tuned.

Protected underscore in inductive_set.

Replaced "hand-made" LaTeX code in Protocol/protocol.tex by generated files in Protocol/document.

Removed legacy ML files in Protocol case study.

LaTeX code is now generated directly from theory files.

Ported ML proof scripts to Isar.

hide internal structures (again);

marked some CRITICAL sections (for multithreading);

added compatibility file for ML systems without multithreading;

interpretation: unfolding of equations;

interpretation: equations are propositions not pairs of terms;

interpretation: unfolding of equations; interpretation: equations are propositions not pairs of terms;

increase default max heap size for poly to -H 500 (this is what isatest uses, -H 80 is not enough for HOL on at-mac-poly).

simultaneous use_thys;

fixed document;

turned ex/prop.ML, ex/quant.ML into proper theories;

inform_file_processed: tuned msg, no state;

simultaneous use_thys;

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;

added ISABELLE_FILE_IDENT;

simplified ThyLoad interfaces: only one additional directory; require_thy: cumulative appending of directory prefix; tuned;

simplified ThyLoad interfaces: only one additional directory; recovered usualy load_path semantics: only basic names are looked up;

simplified ThyLoad interfaces: only one additional directory;

new functions cut_matrix', etc.

dropped Nat.ML legacy bindings

moved class ord from Orderings.thy to HOL.thy