updated;

obsolete;

removed obsolete (slow!) Random implementation;

moved Pure/General/random_word.ML to Tools/random_word.ML;

adapted theory name;

* Metis prover an order of magnitude faster, works with multithreading.

updated HOL-Nominal-Examples deps;

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

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;

cond_timeit: added message argument;

note in target

maior tuning

tuned

Added foldl1.

Adapted to changes in size function.

size functions for nested datatypes are now expressed using generic ..._size functions.

Adapted to changes in interface of indtac.

- Removed redundant head_len field in datatype_info - Added new alt_names field in datatype_info

- Removed redundant head_len field in datatype_info - Added new alt_names field in datatype_info - indtac now takes additional list of variables as argument

tidied some messy proofs

Deleted copy of indtac.

Added code lemma for message_string_size.

Removed obsolete lemma size_sum.

fixed ancestors

whitespace typo

explicit closing of derived witnesses

closed rules