made refute non-critical (seems to work after avoiding floating point random numbers);

move bottom-related stuff back into Pcpo.thy

polishing of some proofs

Random.range_real makes SML/NJ happy;

tuned comments;

tuned RandomWord signature;

removed strange MacRoman character;

using RandomWord from Isabelle/Pure gains factor 10-20 speedup;

updated;

added General/random_word.ML;

Simple generator for pseudo-random numbers, using unboxed word arithmetic only.

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