src/Tools/quickcheck.ML
2013-05-15 wenzelm clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
2013-05-15 wenzelm maintain ProofGeneral preferences within ProofGeneral module;
2013-05-15 wenzelm just one ProofGeneral module;
2013-04-09 wenzelm discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
2013-03-27 wenzelm more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
2013-02-28 wenzelm tuned whitespace and indentation;
2012-11-25 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-09-14 wenzelm clarified markup names;
2012-04-19 haftmann dropped dead code
2012-04-19 haftmann dropped dead code;
2012-04-06 wenzelm standardized alias;
2012-04-04 bulwahn added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
2012-03-16 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 wenzelm prefer formally checked @{keyword} parser;
2012-03-10 bulwahn adding tags to quickcheck's result
2012-03-02 bulwahn collecting all axioms in a locale context in quickcheck;
2012-02-21 bulwahn subtype preprocessing in Quickcheck;
2012-02-14 bulwahn adding abort_potential configuration in Quickcheck
2012-01-27 bulwahn adding some basic handling that unfolds a conjecture in a locale before testing it with quickcheck
2011-12-05 bulwahn making the default behaviour of quickcheck a little bit less verbose;
2011-12-05 bulwahn adding verbose configuration to quickcheck
2011-12-05 bulwahn renaming potential flag to genuine_only flag with an inverse semantics
2011-12-05 bulwahn outputing the potentially spurious counterexample and continue search
2011-12-01 bulwahn outputing if counterexample is potentially spurious or not
2011-12-01 bulwahn extending quickcheck's result by the genuine flag
2011-11-30 bulwahn adding parsing of potential configuration to quickcheck command
2011-11-30 bulwahn adding quickcheck's potential configuration
2011-11-28 wenzelm separate module for concrete Isabelle markup;
2011-11-11 bulwahn adding option allow_function_inversion to quickcheck options
2011-11-09 bulwahn quickcheck fails with code generator errors only if one tester is invoked
2011-11-09 bulwahn removing extra arguments
2011-10-31 bulwahn tuned
2011-10-20 bulwahn adding depth as an quickcheck configuration
2011-10-17 bulwahn 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-07-20 bulwahn removing inner time limits in quickcheck
2011-07-20 bulwahn exporting function in quickcheck; adapting mutabelle script
2011-07-18 bulwahn quickcheck does not deactivate testers if none are given
2011-07-18 bulwahn adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
2011-07-18 bulwahn renaming quickcheck_tester to quickcheck_batch_tester; tuned
2011-07-18 bulwahn changing parser in quickcheck to activate and deactivate the testers
2011-07-18 bulwahn enabling parallel execution of testers but removing more informative quickcheck output
2011-07-18 bulwahn changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
2011-07-18 bulwahn removing generator registration
2011-07-18 bulwahn parametrized test_term functions in quickcheck
2011-07-18 bulwahn adding random, exhaustive and SML quickcheck as testers
2011-07-11 wenzelm tuned signature -- corresponding to Scala version;
2011-06-28 bulwahn adding timeout to quickcheck narrowing
2011-06-09 bulwahn adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
2011-06-02 bulwahn moving the distinction between invocation of testers and generators into test_goal_terms function in quickcheck for its usage with mutabelle
2011-05-31 bulwahn Quickcheck Narrowing only requires one compilation with GHC now
2011-05-31 bulwahn splitting test_goal_terms in Quickcheck into smaller basic functions
2011-05-31 bulwahn adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing
2011-05-27 blanchet use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
2011-05-27 blanchet prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
2011-05-27 blanchet added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
2011-05-27 blanchet renamed "Auto_Tools" "Try"
2011-05-02 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
2011-04-20 bulwahn handling the case where quickcheck is used in a locale with no known interpretation user-friendly
2011-04-16 wenzelm modernized structure Proof_Context;
2011-04-07 bulwahn removing decrement of cardinality in quickcheck -- counting cardinalities starts at 1
less more (0) -100 -60 tip