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);