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;