2009-11-11 haftmann 2009-11-11 adding code equations for constructors
2009-11-11 haftmann 2009-11-11 tuned
2009-11-11 boehmes 2009-11-11 changed URL of SMT server, added Z3 rewrite lemma
2009-11-11 paulson 2009-11-11 Added two new lemmas
2009-11-11 haftmann 2009-11-11 tuned imports
2009-11-11 haftmann 2009-11-11 tuned
2009-11-11 wenzelm 2009-11-11 local mutex for theory content/identity operations;
2009-11-11 wenzelm 2009-11-11 admit dummy implementation;
2009-11-10 wenzelm 2009-11-10 Toplevel.thread provides Isar-style exception output;
2009-11-10 wenzelm 2009-11-10 generalized Runtime.toplevel_error wrt. output function;
2009-11-10 wenzelm 2009-11-10 exported SimpleThread.attributes;
2009-11-10 wenzelm 2009-11-10 plain add_preference, no setmp_CRITICAL required;
2009-11-10 wenzelm 2009-11-10 adapted Theory_Data;
2009-11-10 wenzelm 2009-11-10 recovered update from 7264824baf66, which got lost in 7264824baf66;
2009-11-10 wenzelm 2009-11-10 merged
2009-11-10 haftmann 2009-11-10 merged
2009-11-10 haftmann 2009-11-10 tuned header
2009-11-10 haftmann 2009-11-10 substantial simplification restores code generation
2009-11-10 haftmann 2009-11-10 lemmas about apfst and apsnd
2009-11-10 haftmann 2009-11-10 tuned imports
2009-11-10 huffman 2009-11-10 merged
2009-11-10 huffman 2009-11-10 HOLCF example: domain package proofs done manually
2009-11-10 huffman 2009-11-10 add lemma parallel_fix_ind
2009-11-10 huffman 2009-11-10 add title/author block
2009-11-10 huffman 2009-11-10 theory of representable cpos
2009-11-09 huffman 2009-11-09 add map_map lemmas
2009-11-09 huffman 2009-11-09 add in_deflation relation, more lemmas about cast
2009-11-09 huffman 2009-11-09 ep_pair and deflation lemmas for powerdomain map functions
2009-11-10 blanchet 2009-11-10 remove spurious parameter to "merge"
2009-11-10 blanchet 2009-11-10 merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
2009-11-10 blanchet 2009-11-10 fixed soundness bug in Nitpick related to sets of sets; (detected thanks to the TPTP)
2009-11-05 blanchet 2009-11-05 added possibility to register datatypes as codatatypes in Nitpick; this is useful if the datatype is used only as a means to define the codatatype
2009-11-05 blanchet 2009-11-05 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
2009-11-05 blanchet 2009-11-05 don't promise too much in the Nitpick manual
2009-11-05 blanchet 2009-11-05 merged
2009-11-05 blanchet 2009-11-05 added "nitpick_def" attribute to lfp/gfp definition generated by the inductive package; this ensures that Nitpick can find the definition and determine whether its inductive or coinductive
2009-10-29 blanchet 2009-10-29 merged
2009-10-29 blanchet 2009-10-29 try very hard to remove temporary files generated by Nitpick in case of interruption
2009-10-29 blanchet 2009-10-29 eliminate two FIXMEs in Nitpick's monotonicity check code
2009-10-29 blanchet 2009-10-29 rename "NitpickMono" to "Nitpick_Mono" in example
2009-10-29 blanchet 2009-10-29 merged
2009-10-29 blanchet 2009-10-29 minor cleanup in Nitpick
2009-10-29 blanchet 2009-10-29 make "auto" SAT solver less verbose
2009-10-29 blanchet 2009-10-29 make "sizechange_tac" slightly less verbose
2009-10-29 blanchet 2009-10-29 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
2009-10-29 blanchet 2009-10-29 readded Predicate_Compile to Main
2009-10-29 blanchet 2009-10-29 merged
2009-10-29 blanchet 2009-10-29 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
2009-10-29 blanchet 2009-10-29 fixed minor problems with Nitpick's documentation
2009-10-28 blanchet 2009-10-28 merged
2009-10-28 blanchet 2009-10-28 merged my Auto Nitpick change with Lukas's Predicate Compiler changes
2009-10-28 blanchet 2009-10-28 introduced Auto Nitpick in addition to Auto Quickcheck; this required generalizing the theorem hook used by Quickcheck, following a suggestion by Florian
2009-10-28 blanchet 2009-10-28 use "get_goal" rather than "flat_goal" in Auto Quickcheck, since we don't need the extra facts for counterexample generation
2009-10-27 blanchet 2009-10-27 fix typo in Nitpick manual
2009-10-27 blanchet 2009-10-27 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
2009-10-27 blanchet 2009-10-27 clean Nitpick's wellfoundedness cache once in a while, to avoid potential memory leak
2009-10-27 blanchet 2009-10-27 renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
2009-11-10 wenzelm 2009-11-10 eliminated some old uses of cumulative prems (!) in proof methods;
2009-11-10 wenzelm 2009-11-10 eliminated some unused/obsolete Args.bang_facts;
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;