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;