tuned header; use plain simultaneous lemma statements -- Pure's &&& should hardly ever occur in user space;

made SML/NJ happy; normalized type abbreviations;

eliminated funny record patterns and made SML/NJ happy;

proper header; eliminated SML97's opaque signature constrain, which is essentially a legacy feature (due to problems with ML toplevel pretty printing);

more accurate dependencies; tuned;

merged

added Tree23 to IsaMakefile

New

merged

fixed order of parameters in induction rules

added bulwahn to isatest mailings

merged

Completely overhauled

better error handling for fixrec_simp

add more fixrec_simp rules

fixrec examples use fixrec_simp instead of fixpat

domain package registers fixrec_simp lemmas

merged

add fixrec_simp attribute and method (eventually to replace fixpat)

proper and unique case names for the split_vc method, shortened label names, added an example demonstrating the split_vc method

merged

merged

always be qualified -- suspected smartness in fact never worked as expected

pretty name for ==>

added HOL-Boogie

added a specific SMT exception captured by smt_tac (prevents the SMT method from failing with an exception), replaced unspecific 'error' invocations with raising of specific SMT exceptions, added annotations to traced SMT problem and solver output

ignore parsing errors, return empty assignment instead

scheduler: clarified interrupt attributes and handling;

worker_next: plain signalling via work_available only, not scheduler_event; scheduler: tuned worker pool adjustments;

revert fulfill_proof_future tuning (actually a bit slower due to granularity issues?);

avoid broadcast work_available, use daisy-chained signal instead; max_threads: allow as much as 4 * m, after extra delay;

fulfill_proof_future: tuned important special case of singleton promise;

worker_next: treat wait for work_available as Sleeping, not Waiting; max_threads: simple adaptive scheme between m and 2 * m;

worker activity: distinguish between waiting (formerly active) and sleeping; tuned;

tuned;

tuned thread data;

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;

less verbose termination tactics

less verbose inductive invocation

tuned

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