2007-08-01 wenzelm 2007-08-01 tuned config options: eliminated separate attribute "option";
2007-08-01 wenzelm 2007-08-01 oops -- fixed syntax;
2007-08-01 wenzelm 2007-08-01 "running": PROTECTED wakeup; "cont": actually invoke wakeup!!
2007-07-31 wenzelm 2007-07-31 proper path specifications;
2007-07-31 wenzelm 2007-07-31 simultaneous use_thys;
2007-07-31 wenzelm 2007-07-31 setmp_noncritical print_mode;
2007-07-31 wenzelm 2007-07-31 simultaneous use_thys;
2007-07-31 wenzelm 2007-07-31 removed obsolete HOL/Real/ROOT.ML;
2007-07-31 wenzelm 2007-07-31 no_document: setmp_noncritical;
2007-07-31 wenzelm 2007-07-31 with_charset: setmp_noncritical;
2007-07-31 wenzelm 2007-07-31 added max-threads preference;
2007-07-31 wenzelm 2007-07-31 replaced depth_limit ref by blast_depth_limit configuration option; tuned method setup;
2007-07-31 wenzelm 2007-07-31 replaced dtK ref by datatype_distinctness_limit configuration option;
2007-07-31 wenzelm 2007-07-31 moved classical tools from theory IFOL to FOL;
2007-07-31 wenzelm 2007-07-31 register_thy: more sanity checks;
2007-07-31 wenzelm 2007-07-31 moved lin_arith stuff to Tools/lin_arith.ML;
2007-07-31 wenzelm 2007-07-31 proper context for cooper_tac within arith;
2007-07-31 wenzelm 2007-07-31 tuned LinArith setup;
2007-07-31 wenzelm 2007-07-31 HOL setup for linear arithmetic -- moved here from arith_data.ML;
2007-07-31 wenzelm 2007-07-31 added Tools/lin_arith.ML;
2007-07-31 wenzelm 2007-07-31 tuned;
2007-07-31 wenzelm 2007-07-31 tuned section "Style"; added section "Thread-safe programming";
2007-07-31 narboux 2007-07-31 undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
2007-07-31 ballarin 2007-07-31 Proper interpretation of total orders in lattices.
2007-07-31 wenzelm 2007-07-31 * Configuration options; * Named collections of theorems;
2007-07-31 wenzelm 2007-07-31 added configuration options;
2007-07-31 wenzelm 2007-07-31 removed use/update_thy_only;
2007-07-31 chaieb 2007-07-31 find_body goes under meta-quantifier ; tactic generalizes free variables;
2007-07-31 chaieb 2007-07-31 Added dependency on langford files in Tools/Qelim
2007-07-31 chaieb 2007-07-31 Tuned document
2007-07-31 wenzelm 2007-07-31 added register_thy (replaces pretend_use_thy_only and really flag); tuned;
2007-07-31 wenzelm 2007-07-31 ThyInfo.register_thy;
2007-07-31 wenzelm 2007-07-31 turned fast_arith_split/neq_limit into configuration options;
2007-07-31 wenzelm 2007-07-31 added global config options;
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context; turned fast_arith_split/neq_limit into configuration options; tuned signatures; misc cleanup;
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context;
2007-07-30 wenzelm 2007-07-30 tuned ML declarations;
2007-07-30 wenzelm 2007-07-30 simultaneous use_thys; tuned;
2007-07-30 wenzelm 2007-07-30 dequeue: wait loop while PROTECTED -- avoids race condition;
2007-07-30 wenzelm 2007-07-30 marked some CRITICAL sections;
2007-07-30 urbanc 2007-07-30 updated some of the definitions and proofs
2007-07-29 wenzelm 2007-07-29 tuned msgs; tuned;
2007-07-29 wenzelm 2007-07-29 deps: keep thy source text, avoid reloading; schedule: pick the first task with maximal imm_succs;
2007-07-29 wenzelm 2007-07-29 adapted ThyLoad.deps_thy;
2007-07-29 wenzelm 2007-07-29 more informative tracing; tuned;
2007-07-29 wenzelm 2007-07-29 load_thy: avoid reloading of text; tuned;
2007-07-29 wenzelm 2007-07-29 added of_list_limited (with limit argument); removed of_string_limited;
2007-07-29 wenzelm 2007-07-29 more informative tracing;
2007-07-29 wenzelm 2007-07-29 explicit global state argument -- no longer CRITICAL;
2007-07-29 wenzelm 2007-07-29 added option -T (multithreading trace mode);
2007-07-29 wenzelm 2007-07-29 critical: improved diagostics; schedule: proper broadcast on wakeup condition;
2007-07-29 wenzelm 2007-07-29 tuned msg;
2007-07-29 wenzelm 2007-07-29 NAMED_CRITICAL;
2007-07-29 wenzelm 2007-07-29 removed obsolete Output.ML_errors/toplevel_errors; moved ML toplevel use commands to pure_setup.ML;
2007-07-29 wenzelm 2007-07-29 removed obsolete Output.ML_errors/toplevel_errors;
2007-07-29 wenzelm 2007-07-29 added TOPLEVEL_ERROR (simplified version from output.ML);
2007-07-29 wenzelm 2007-07-29 removed obsolete TOPLEVEL_ERROR etc. (cf. toplevel.ML);
2007-07-29 wenzelm 2007-07-29 added ML toplevel use commands: Toplevel.program; added install_pp stuff;
2007-07-29 wenzelm 2007-07-29 removed obsolete install_pp.ML (cf. pure_setup.ML);
2007-07-29 wenzelm 2007-07-29 replaced program_defs_ref by proper context data (via attribute "program");