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;

less verbose termination tactics

less verbose inductive invocation

tuned

absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned