removed duplicate CRITICAL markup;

instantiation target

tuned primitive inferences

Replaced refs by config params; finer critical section in mets method

simultaneous use_thys;

marked refute (the main metis procedure) as CRITICAL;

more examples

accomodate to replacement of K_record by %x.c

replaced K_record by lambda term %x. c

signature BASIC_MULTITHREADING; added specific serial number generator, which avoid the global CRITICAL lock;

removed obsolete use_noncritical (plain use is already non-critical);

serial: now based on specific version in structure Multithreading;

add class ppo of pointed partial orders; define UU in class ppo instead of pcpo; add new lemmas about lub

named some critical sections; eval_antiquotes: tightened critical section;

named some critical sections;

use_text/use_file: non-critical (Poly/ML compiler is thread-safe);

non-critical (accidental concurrent access does not affect functional integrity);

PrintMode.setmp (avoid direct access to print_mode ref);

rearrange into subsections

Skolemization now catches exception THM, which may be raised if unification fails.

Deleted redundant setmp calls

tuned proofs, document;

switched from PreList to ATP_Linkup

Renamed *.size to prod.size.

Alternative names are now also used when storing theorems for size functions.

temporarily fixed documentation due to changed size functions

split_primel: salvaged original proof after blow with sledghammer (this constructive version is required in HOL/Extraction);

cond_timeit: added message argument, use Exn.capture/release; tuned;