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

added ML toplevel use commands: Toplevel.program; added install_pp stuff;

removed obsolete install_pp.ML (cf. pure_setup.ML);

replaced program_defs_ref by proper context data (via attribute "program");

renamed Drule.is_dummy_thm to Thm.is_dummy;

added list update;

moved Drule.add/del/merge_rules to Thm.add/del/merge_thms; moved Drule.is_dummy_thm to Thm.is_dummy;

Named collections of theorems in canonical order.

added Tools/named_thms.ML;

renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms; tuned;

avoid ill-defined Simp_tac;

marked some CRITICAL sections;

simplified ResAtpset via NamedThmsFun;

metis_tac: proper context (ProofContext.init it *not* sufficient); simplified method setup;

proper simproc_setup for "neq", "let_simp"; removed dead code;

renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;

replaced make_imp by rev_mp;

proper simproc_setup for "list_neq";

removed obsolete Tools/res_atpset.ML;

simplified ResAtpset via NamedThmsFun; proper simproc_setup for "neq", "let_simp";

simplified "eval" setup via NamedThmsFun;

tuned;

* Isar: command 'declaration'; * Isar: proper interfaces for simplification procedures; * Isar: an extra pair of brackets around attribute declarations abbreviates a theorem reference involving an internal dummy fact;

type Morphism.declaration;

attribute "option": proper naming within the theory

removed dead code;

declaration: proper naming within the theory;

use config_option.ML after sign.ML;

commands 'declare', 'declaration';

added :|-- (dependent projection); tuned;

added attribute "simproc"; marked some CRITICAL sections; tuned;

setmp: NAMED_CRITICAL;

tuned;

added get_cs/map_cs;

tuned signature;

tuned ML/simproc declarations;

removed redundant simproc declarations;

simproc_setup fun_upd2;

added [[decl]] notation;

added command 'simproc_setup', attribute "simproc";

attribs: not cut (!!!);

xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);

get_thm etc.: map empty name to dummy_thm;

chain/using: filter out dummy_thm;

method section scanners: added [[declaration]] syntax, ignore sid-effects of thms;

renamed Config to ConfigOption;

renamed Config to ConfigOption; thm scanners: added [[declaration]] syntax (abbreviates dummy_thm [att]);

renamed config.ML to config_option.ML;

Druke.dummy_thm;

added dummy_thm, is_dummy_thm;

map_value: dynamic type checking;

attribute "option": more elaborate syntax (with value parsing);

added terminator, named_attribute;

exported datatype value; added the_config; removed put_generic_src -- moved value parsing to attrib.ML; tuned;

no 'nat' is needed for Bound in reification

*** empty log message ***

added cases

Updated proofs;

Updated reification : CX discontinued for CN

Updated proofs; changed shadow syntax to improve (processing) time

removed redundant ilcm_dvd1 ilcm_dvd2 zvdd_abs1

fixed broken proof

updated;

renamed CRITICAL' to NAMED_CRITICAL; tuned messages;

renamed CRITICAL' to NAMED_CRITICAL;

added command 'print_options';

added attribute "option" for setting configuration options;

Configuration options as values within the local context.

added config.ML;

NAMED_CRITICAL;

fixed broken proof

Added lemmas

require_thy/schedule: improved task graph, actually observe dependencies on running tasks;

added trace flag, official tracing operation; added named CRITICAL'; schedule: tuned signature, actually observe dependencies on running tasks;

added structure Task; added trace flag, official tracing operation; added named CRITICAL'; schedule: tuned signature;

Secure.use_noncritical root;

added use_noncritical;

tuned

fixed proofs involving dvd;

*** empty log message ***

require_thy: tuned tasks graph, removed visited; use_thy etc.: schedule for multithreading;

renamed number_of_threads to max_threads; added schedule operator;

added usedir option -M: max threads;

renamed lemma "set_take_whileD" to "set_takeWhileD"