worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock); worker_start: back to non-self version; scheduler: status output based on ticks;

slightly leaner and more direct control of worker activity etc.;

adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example

adapted the inlining in the predicate compiler

recursively replacing abstractions by new definitions in the predicate compiler

merge

add fixrec support for HOL pair constructor patterns

define cprod_fun using Pair instead of cpair

add (LAM (x, y). t) syntax and lemma csplit_Pair

lexicographic order: run local descent proofs in parallel

merged

domain package no longer uses cfst/csnd/cpair

conceal partial rules depending on config flag (i.e. when called via "fun")

conceal "termination" rule, used only by special tools

do not use Binding.empty: conceal flag gets lost in Thm.def_binding_optional

modernized structure XML_Syntax;

structure Thm_Deps;

modernized structure Proof_Node;

modernized structure Proof_Display;

modernized structure Proof_Syntax;

modernized structure Local_Syntax;

modernized structure AutoBind;

modernized structure Primitive_Defs;

modernized structure Simple_Syntax;

modernized structure Context_Position;

observe usual naming conventions;

find_theorems: respect conceal flag

DEEPEN: all tracing is subject to trace_DEEPEN (NB: Proof General tends to "popup" tracing output);

back to warning -- Proof General tends to "popup" tracing output;

split parsing of counterexamples from translation into terms (avoids Term.dummyT and ill-typed terms)

merged

predicate compiler creates code equations for predicates with full mode

renamed rpred to random

Rules that characterize functional/relational specifications.

adapted Item_Net; tuned;

allow multi-index; more scalable merge; renamed delete to remove, and insert to update (standard naming conventions); tuned;

added insert_safe, delete_safe variants;

tuned signature;

modernized structure Context_Rules;

modernized structure Rule_Cases;

merged

dedicated theory for loading numeral simprocs

set Pure theory name properly

tuned code setup

some notes on SPASS 3.0 distribution;

merged

combined former theories Divides and IntDiv to one theory Divides

tuned variable names of bindings; conceal predicate constants

dedicated theory for loading numeral simprocs

moved some div/mod lemmas to theory Divides

tuned proof

moved Commutative_Ring into session Decision_Procs

abstract over variables in reversed order (application uses given order)

disable printing of unparsed counterexamples for CVC3 and Yices

pattern are separated only by spaces (no comma)

back to polyml-svn -- performance impact is minimal, slowdown was caused by accumulated cruft of long-running Mac OS;