2009-11-05 wenzelm misc tuning and clarification;
2009-11-05 wenzelm scalable version of Named_Thms, using Item_Net;
2009-11-05 wenzelm merged
2009-11-05 wenzelm merged
2009-11-05 wenzelm more accurate cleanup;
2009-11-05 wenzelm merged
2009-11-05 wenzelm more accurate dependencies;
2009-11-05 boehmes merged
2009-11-05 boehmes handle let expressions inside terms by unfolding (instead of raising an exception),
2009-11-05 boehmes shorter names for variables and verification conditions,
2009-11-05 boehmes added references to HOL-Boogie papers
2009-11-05 wenzelm tuned header;
2009-11-05 wenzelm made SML/NJ happy;
2009-11-05 wenzelm eliminated funny record patterns and made SML/NJ happy;
2009-11-05 wenzelm proper header;
2009-11-05 wenzelm more accurate dependencies;
2009-11-05 wenzelm merged
2009-11-04 krauss added Tree23 to IsaMakefile
2009-11-04 nipkow New
2009-11-04 nipkow merged
2009-11-04 nipkow fixed order of parameters in induction rules
2009-11-04 krauss added bulwahn to isatest mailings
2009-11-04 nipkow merged
2009-11-04 nipkow Completely overhauled
2009-11-04 huffman better error handling for fixrec_simp
2009-11-04 huffman add more fixrec_simp rules
2009-11-04 huffman fixrec examples use fixrec_simp instead of fixpat
2009-11-04 huffman domain package registers fixrec_simp lemmas
2009-11-04 huffman merged
2009-11-04 huffman add fixrec_simp attribute and method (eventually to replace fixpat)
2009-11-03 boehmes proper and unique case names for the split_vc method,
2009-11-03 haftmann merged
2009-11-03 haftmann merged
2009-11-03 haftmann always be qualified -- suspected smartness in fact never worked as expected
2009-11-03 haftmann pretty name for ==>
2009-11-03 boehmes added HOL-Boogie
2009-11-03 boehmes added a specific SMT exception captured by smt_tac (prevents the SMT method from failing with an exception),
2009-11-03 boehmes ignore parsing errors, return empty assignment instead
2009-11-05 wenzelm scheduler: clarified interrupt attributes and handling;
2009-11-05 wenzelm worker_next: plain signalling via work_available only, not scheduler_event;
2009-11-04 wenzelm revert fulfill_proof_future tuning (actually a bit slower due to granularity issues?);
2009-11-04 wenzelm avoid broadcast work_available, use daisy-chained signal instead;
2009-11-04 wenzelm fulfill_proof_future: tuned important special case of singleton promise;
2009-11-04 wenzelm worker_next: treat wait for work_available as Sleeping, not Waiting;
2009-11-04 wenzelm worker activity: distinguish between waiting (formerly active) and sleeping;
2009-11-04 wenzelm tuned;
2009-11-04 wenzelm tuned thread data;
2009-11-03 wenzelm worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
2009-11-03 wenzelm slightly leaner and more direct control of worker activity etc.;
2009-11-03 bulwahn adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
2009-11-03 bulwahn adapted the inlining in the predicate compiler
2009-11-03 bulwahn recursively replacing abstractions by new definitions in the predicate compiler
2009-11-03 huffman merge
2009-11-03 huffman add fixrec support for HOL pair constructor patterns
2009-11-03 huffman define cprod_fun using Pair instead of cpair
2009-11-03 huffman add (LAM (x, y). t) syntax and lemma csplit_Pair
2009-11-02 krauss lexicographic order: run local descent proofs in parallel
2009-11-02 huffman merged
2009-11-02 huffman domain package no longer uses cfst/csnd/cpair
2009-11-02 krauss conceal partial rules depending on config flag (i.e. when called via "fun")
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip