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");
2007-07-29 wenzelm 2007-07-29 renamed Drule.is_dummy_thm to Thm.is_dummy;
2007-07-29 wenzelm 2007-07-29 added list update;
2007-07-29 wenzelm 2007-07-29 moved Drule.add/del/merge_rules to Thm.add/del/merge_thms; moved Drule.is_dummy_thm to Thm.is_dummy;
2007-07-29 wenzelm 2007-07-29 Named collections of theorems in canonical order.
2007-07-29 wenzelm 2007-07-29 added Tools/named_thms.ML;
2007-07-29 wenzelm 2007-07-29 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms; tuned;
2007-07-29 wenzelm 2007-07-29 avoid ill-defined Simp_tac;
2007-07-29 wenzelm 2007-07-29 marked some CRITICAL sections;
2007-07-29 wenzelm 2007-07-29 simplified ResAtpset via NamedThmsFun;
2007-07-29 wenzelm 2007-07-29 metis_tac: proper context (ProofContext.init it *not* sufficient); simplified method setup;
2007-07-29 wenzelm 2007-07-29 proper simproc_setup for "neq", "let_simp"; removed dead code;
2007-07-29 wenzelm 2007-07-29 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-07-29 wenzelm 2007-07-29 replaced make_imp by rev_mp;
2007-07-29 wenzelm 2007-07-29 proper simproc_setup for "list_neq";
2007-07-29 wenzelm 2007-07-29 removed obsolete Tools/res_atpset.ML;
2007-07-29 wenzelm 2007-07-29 simplified ResAtpset via NamedThmsFun; proper simproc_setup for "neq", "let_simp";
2007-07-29 wenzelm 2007-07-29 simplified "eval" setup via NamedThmsFun;