2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-07-17 bulwahn 2012-07-17 improved equality optimisation in Quickcheck
2012-03-17 wenzelm 2012-03-17 'definition' no longer exports the foundational "raw_def";
2012-03-17 wenzelm 2012-03-17 some attempts to fit source on screen;
2012-02-24 haftmann 2012-02-24 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24 haftmann 2012-02-24 given up disfruitful branch
2012-02-23 haftmann 2012-02-23 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-20 huffman 2012-02-20 use qualified constant names instead of suffixes (from Florian Haftmann)
2012-01-23 bulwahn 2012-01-23 random instance for sets
2011-12-09 bulwahn 2011-12-09 hiding definitional facts in Quickcheck; introducing catch_match more honestly
2011-12-01 bulwahn 2011-12-01 hiding internal constants and facts more properly
2011-12-01 bulwahn 2011-12-01 making catch_match polymorphic
2011-12-01 bulwahn 2011-12-01 quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
2011-12-01 bulwahn 2011-12-01 quickcheck random can also find potential counterexamples; moved catch_match definition; split quickcheck setup;
2011-10-19 bulwahn 2011-10-19 removing quickcheck tester SML-inductive based on the old code generator
2011-10-17 bulwahn 2011-10-17 moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
2011-09-09 krauss 2011-09-09 added syntactic classes for "inf" and "sup"
2011-03-30 bulwahn 2011-03-30 removing junk that should not have been committed
2011-03-30 bulwahn 2011-03-30 renewing specifications in HOL: replacing types by type_synonym
2011-03-30 bulwahn 2011-03-30 generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
2011-03-11 bulwahn 2011-03-11 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
2011-03-11 bulwahn 2011-03-11 adaptions in generators using the common functions
2011-03-11 bulwahn 2011-03-11 renaming signatures and structures; correcting header
2011-03-11 bulwahn 2011-03-11 adapting Quickcheck theory after moving ML files
2010-12-06 bulwahn 2010-12-06 removing declaration in quickcheck to really enable exhaustive testing
2010-12-03 bulwahn 2010-12-03 declaring quickcheck testers as default after their setup
2010-11-22 bulwahn 2010-11-22 adding Enum to HOL-Main image and removing it from HOL-Library
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-07-09 haftmann 2010-07-09 nicer xsymbol syntax for fcomp and scomp
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-31 bulwahn 2010-03-31 adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
2010-03-22 bulwahn 2010-03-22 a new simpler random compilation for the predicate compiler
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-27 haftmann 2010-01-27 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
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-27 bulwahn 2009-10-27 hiding randompred definitions
2009-10-27 bulwahn 2009-10-27 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
2009-09-23 haftmann 2009-09-23 Code_Eval(uation)
2009-08-14 haftmann 2009-08-14 formally stylized
2009-07-10 haftmann 2009-07-10 tuned quickcheck generator for bool
2009-06-15 haftmann 2009-06-15 hide constant Quickcheck.random
2009-06-13 haftmann 2009-06-13 more convenient signature for random_fun_lift
2009-06-10 haftmann 2009-06-10 tuned order
2009-06-10 haftmann 2009-06-10 revised interpretation combinator for datatype constructions
2009-06-08 haftmann 2009-06-08 added generator for char and trivial generator for String.literal
2009-05-27 haftmann 2009-05-27 added lemma beyond_zero; hide constants
2009-05-26 haftmann 2009-05-26 separate module for quickcheck generators
2009-05-24 haftmann 2009-05-24 merged
2009-05-21 haftmann 2009-05-21 re-added corrected version of type copy quickcheck generator
2009-05-20 haftmann 2009-05-20 removed quickcheck generator for type copies temporarily
2009-05-20 haftmann 2009-05-20 added generator for type copies (records)
2009-05-19 haftmann 2009-05-19 String.literal replaces message_string, code_numeral replaces (code_)index
2009-05-19 haftmann 2009-05-19 moved Code_Index, Random and Quickcheck before Main
2009-05-18 haftmann 2009-05-18 added quickcheck support for numeric types
2009-05-16 haftmann 2009-05-16 experimental move of Quickcheck and related theories to HOL image