add dcpo instance proof

declare upE as cases rule; add new rule up_induct

update sq_ord/po instance proofs

move lemmas from Cont.thy to Ffun.thy; reorder dependency of Cont.thy and Ffun.thy; add dcpo instance proofs for function type

remove not_up_less_UU [simp]

update instance proofs for sq_ord, po; new instance proofs for dcpo

add lemma ub2ub_monofun'

added dcpo instance proofs

new class dcpo; added dcpo versions of some lemmas

added new lemmas

add lemma dir2dir_monofun

tuned;

new is_ub lemmas; new lub syntax for set image

Multithreading.max_threads := 0 refers to number of cores of underlying machine;

added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;

added usedir -M max (alias for -M 0);

new section for directed sets

split of class uminus

empty dictionaries for OCaml

clarified policy

tuned

some more antiquotations

index now a copy of nat rather than int

absolute import

some more primrec

removed some legacy instantiations

improved evaluation mechanism

splitted class uminus from class minus

testing for empty sort

new metis proofs

renamed foldM to fold_mset on general request added Tobias' lemmas on fold_mset (A+B) etc tuned default simp set for fold_mset

update instance proofs to new style

declare sprodE as cases rule; new induction rule sprod_induct

add induction rule ssum_induct

eval_wrapper: CRITICAL; tuned;

try_ml_file: setmp explicit theory context, prevents race condition wrt. concurrent ML_Context.set_context;

tuned spaces;

removed separate exists/forall code;

tuned proofs and comments

removed obsolete banner;

tuned;

added PROMPT message;

added isSystem; tune isRaw;

simple make script;

tuned comments (javadoc);

use polyml-cvs, the 5.2 development branch;

tuned RandomWord interface;

added int/real/list operations; tuned interface; tuned;

use random_word.ML earlier;

changed type definition to make Iwhen and reasoning about chains unnecessary; rearranged sections

Fixed eta constraction issue in compose_witness

included meson/metis tests in simultaneous use_thys;

``print mode'' is now a thread-local value derived from a global template;

scheduling/next_task: PrintMode.closure;

added get/put_data;

separated into global template vs. thread-local value; made setmp thread-local (non-critical); added closure;

Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.

added ML-Systems/universal.ML;

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.