disabled upt example because of a problem due to overloaded constants with the predicate compiler

added optional mode annotations for parameters in the values command

moved values command from core to predicate compile

added further example of the values command

Adopted output of values command

improved handling of overloaded constants; examples with numerals

made SML/NJ happy; tuned

adding tracing function for evaluated code; annotated compilation in the predicate compiler

added documentation for local SMT solver setup and available SMT options, added verbose output for SMT solver invocation, test if local SMT solver exists before invoking it, always trace (possible) counterexamples, documented existence of SMT server

renamed method induct_scheme to induction_schema

NEWS

removed session SizeChange: outdated, only half-functional, alternatives exist (cf. size_change method)

renamed method sizechange to size_change

added boehmes and hoelzl to isatest mailings

merged

tuned

Merged.

Merged.

Use PrintMode.setmp to make thread-safe; avoid code clones.

Make output indenpendent of current print mode.

Relax on type agreement with original context when applying term syntax.

tuned;

proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context; tuned signature; tuned;

adapted LocalTheory.declaration;

allow "pervasive" local theory declarations, which are applied the background theory;

declare Spec_Rules for most basic definitional packages;

misc tuning and clarification;

scalable version of Named_Thms, using Item_Net;

merged

merged

more accurate cleanup;

merged

more accurate dependencies;

merged

handle let expressions inside terms by unfolding (instead of raising an exception), added examples to test this feature

shorter names for variables and verification conditions, auto-fix variables occurring in a verification condition

added references to HOL-Boogie papers

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;