renamed CRITICAL' to NAMED_CRITICAL;

added command 'print_options';

added attribute "option" for setting configuration options;

Configuration options as values within the local context.

added config.ML;

NAMED_CRITICAL;

fixed broken proof

Added lemmas

require_thy/schedule: improved task graph, actually observe dependencies on running tasks;

added trace flag, official tracing operation; added named CRITICAL'; schedule: tuned signature, actually observe dependencies on running tasks;

added structure Task; added trace flag, official tracing operation; added named CRITICAL'; schedule: tuned signature;

Secure.use_noncritical root;

added use_noncritical;

tuned

fixed proofs involving dvd;

*** empty log message ***

require_thy: tuned tasks graph, removed visited; use_thy etc.: schedule for multithreading;

renamed number_of_threads to max_threads; added schedule operator;

added usedir option -M: max threads;

renamed lemma "set_take_whileD" to "set_takeWhileD"

cleaned up the proofs a bit

Added cancel simprocs for dvd on nat and int

renamed to multithreading_dummy.ML;

require_thy: explicit tasks graph; added sequential scheduler; internal tuning;

moved exception capture/release to structure Exn; moved multithreading to multithreading_polyml.ML;

ML-Systems/exn.ML, ML-Systems/multithreading_dummy.ML;

added topological_order; tuned;

moved exception capture/release to structure Exn;

Runtime exceptions as values (from library.ML);

Multithreading in Poly/ML (version 5.1).

Compatibility file for ML systems without multithreading.

renamed ML-Systems/no_multithreading.ML to ML-Systems/multithreading_dummy.ML; added ML-Systems/multithreading_polyml.ML, ML-Systems/exn.ML

marked some CRITICAL sections;

Interpretation of rings (as integers) maps defined operations to defined operations..

updated

added compile_term interface

swapped class projection order

interpretation_in

tuned

renamed lcm_lowest to lcm_least

dropped axclass

using interpretation with derived concepts

using class target

added proper implementation of self_critical, CRITICAL;

added multithreading, self_critical

RAW: updated deps;

marked some CRITICAL sections;

added compatibility wrapper for polyml-5.1;

marked some CRITICAL sections; eliminated transform_failure (to avoid critical section for main transactions);

avoid global reference warned'';

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

dropped Nat.ML legacy bindings

split class abs from class minus

simplified HOL bootstrap

tuned;

ThyHeader.read: Source.of_string_limited;

added of_string_limited (more efficient for partial scans);

added rep_ident;

added pprint for Path.T, File.ident;

tuned signature; load_path: always used, even for partially qualified path names; check_file: precise (no adding of extensions!); misc cleanup;

removed obsolete use/update_thy_only; removed unused quiet_update_thy, get_succs; renamed get_preds to get_parents; deps: replaced File.info by File.ident (no comparison of paths!); check_deps: reload (partially qualified) parents for unfinished theory, no reference of previously loaded master paths! require_thy: attempt at purely static path lookup, less permissive; misc cleanup;