named some CRITICAL sections;

misc cleanup of ML bindings (for multihreading);

added int type constraint to accomodate hacked SML/NJ (backported change in generated metis.ML);

preparations for proper type int;

tuned tracing;

replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref; thread-safeness: when creating certified items, perform Theory.check_thy *last*;

certify: no check_thy here;

improved check_thy: produce a checked theory_ref (thread-safe version); removed obsolete self_ref (cf. check_thy); thread-safeness: when creating certified items, perform Theory.check_thy *last*; eq_thy: no check here; marked some critical sections;

moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;

added dependency on Tools/Metis/metis.ML;

updated;

replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;

reset Logic.auto_rename;

added int type constraints to accomodate hacked SML/NJ;

added int type constraints to accomodate hacked SML/NJ;

added int type constraints to accomodate hacked SML/NJ;

made mk_int/dest_int pervasive;

Experimental removal of assumptions of the form x : UNIV and the like after interpretation.

Repaired term_of_char.

- Added cycle test to function mk_ind_def to avoid non-termination of code generator. - Functions generated from inductive predicates having neither parameters nor input arguments now take a unit element as an argument, otherwise the generated code would be ill-formed.

tuned;

converted Meson tests to proper theory;

turned simp_depth_limit into configuration option; tuned register_config;

added name_of;

turned simp_depth_limit into configuration option;

tuned ML bindings (for multithreading); updated timings;

tuned ML bindings (for multithreading);

fix looping when applied to standard subgoals

updated;

tracing: level;

multithreading trace: int;

added toplevel print command;

tuned;

renamed 'print_options' to 'print_configs';

renamed config_option.ML to config.ML; moved attrib setup to attrib.ML;

renamed config_option.ML to config.ML;

simplified internal Config interface;

updated;

tuned config options: eliminated separate attribute "option";

oops -- fixed syntax;

"running": PROTECTED wakeup; "cont": actually invoke wakeup!!

proper path specifications;

simultaneous use_thys;

setmp_noncritical print_mode;

simultaneous use_thys;

removed obsolete HOL/Real/ROOT.ML;

no_document: setmp_noncritical;

with_charset: setmp_noncritical;

added max-threads preference;

replaced depth_limit ref by blast_depth_limit configuration option; tuned method setup;

replaced dtK ref by datatype_distinctness_limit configuration option;

moved classical tools from theory IFOL to FOL;

register_thy: more sanity checks;

moved lin_arith stuff to Tools/lin_arith.ML;

proper context for cooper_tac within arith;

tuned LinArith setup;

HOL setup for linear arithmetic -- moved here from arith_data.ML;

added Tools/lin_arith.ML;

tuned;

tuned section "Style"; added section "Thread-safe programming";

undo a change in last commit : give a single name to the inversion lemmas for the same inductive type

Proper interpretation of total orders in lattices.

* Configuration options; * Named collections of theorems;

added configuration options;

removed use/update_thy_only;

find_body goes under meta-quantifier ; tactic generalizes free variables;

Added dependency on langford files in Tools/Qelim

Tuned document

added register_thy (replaces pretend_use_thy_only and really flag); tuned;

ThyInfo.register_thy;

turned fast_arith_split/neq_limit into configuration options;

added global config options;

arith method setup: proper context; turned fast_arith_split/neq_limit into configuration options; tuned signatures; misc cleanup;

arith method setup: proper context;

tuned ML declarations;

simultaneous use_thys; tuned;

dequeue: wait loop while PROTECTED -- avoids race condition;

marked some CRITICAL sections;

updated some of the definitions and proofs

tuned msgs; tuned;

deps: keep thy source text, avoid reloading; schedule: pick the first task with maximal imm_succs;

adapted ThyLoad.deps_thy;

more informative tracing; tuned;

load_thy: avoid reloading of text; tuned;

added of_list_limited (with limit argument); removed of_string_limited;

more informative tracing;

explicit global state argument -- no longer CRITICAL;

added option -T (multithreading trace mode);

critical: improved diagostics; schedule: proper broadcast on wakeup condition;

tuned msg;

NAMED_CRITICAL;

removed obsolete Output.ML_errors/toplevel_errors; moved ML toplevel use commands to pure_setup.ML;

removed obsolete Output.ML_errors/toplevel_errors;

added TOPLEVEL_ERROR (simplified version from output.ML);

removed obsolete TOPLEVEL_ERROR etc. (cf. toplevel.ML);

added ML toplevel use commands: Toplevel.program; added install_pp stuff;