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