src/Tools/quickcheck.ML
17 months ago wenzelm 2017-12-06 prefer control symbol antiquotations;
2016-04-14 wenzelm 2016-04-14 avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
2016-04-14 wenzelm 2016-04-14 tuned;
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2015-07-06 wenzelm 2015-07-06 tuned message;
2015-04-22 wenzelm 2015-04-22 allow diagnostic proof commands with skip_proofs;
2015-04-16 wenzelm 2015-04-16 explicit error for Toplevel.proof_of; eliminated obsolete Toplevel.unknown_proof; more total Toplevel.proof_position_of;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-01-25 wenzelm 2015-01-25 tuned;
2015-01-25 wenzelm 2015-01-25 more compact message;
2015-01-25 wenzelm 2015-01-25 proper naming convention;
2015-01-25 wenzelm 2015-01-25 prefer plain tuples;
2015-01-25 wenzelm 2015-01-25 tuned message;
2014-12-23 wenzelm 2014-12-23 explicit message channels for "state", "information"; separate state_message_color;
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-11-03 wenzelm 2014-11-03 eliminated obsolete Proof.goal_message -- print outcome more directly;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete Output.urgent_message;
2014-10-31 wenzelm 2014-10-31 discontinued Proof General;
2014-06-08 haftmann 2014-06-08 recovered level-free fishing for locale, accidentally lost in dce365931721
2014-06-07 haftmann 2014-06-07 less baroque interface
2014-04-08 wenzelm 2014-04-08 more uniform ML/document antiquotations;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-02-20 wenzelm 2014-02-20 tuned;
2014-02-20 wenzelm 2014-02-20 proper naming convention;
2014-02-20 wenzelm 2014-02-20 tuned whitespace;
2013-07-17 wenzelm 2013-07-17 tuned message;
2013-07-13 wenzelm 2013-07-13 clarified some default options;
2013-07-13 wenzelm 2013-07-13 more explicit Markup.information for messages produced by "auto" tools;
2013-07-13 wenzelm 2013-07-13 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
2013-07-12 wenzelm 2013-07-12 system options for Isabelle/HOL proof tools;
2013-05-15 wenzelm 2013-05-15 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 2013-05-15 maintain ProofGeneral preferences within ProofGeneral module; initialize Isabelle/Pure preferences within normal user space (with antiquotations); tuned;
2013-05-15 wenzelm 2013-05-15 just one ProofGeneral module;
2013-04-09 wenzelm 2013-04-09 discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;
2013-03-27 wenzelm 2013-03-27 more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
2013-02-28 wenzelm 2013-02-28 tuned whitespace and indentation;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-09-14 wenzelm 2012-09-14 clarified markup names;
2012-04-19 haftmann 2012-04-19 dropped dead code
2012-04-19 haftmann 2012-04-19 dropped dead code; tuned
2012-04-06 wenzelm 2012-04-06 standardized alias;
2012-04-04 bulwahn 2012-04-04 added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck; added examples of quickcheck_locale option; trying to speed up Quickcheck_Examples;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 wenzelm 2012-03-15 prefer formally checked @{keyword} parser;
2012-03-10 bulwahn 2012-03-10 adding tags to quickcheck's result
2012-03-02 bulwahn 2012-03-02 collecting all axioms in a locale context in quickcheck; adding some verbose output;
2012-02-21 bulwahn 2012-02-21 subtype preprocessing in Quickcheck; adding option use_subtype; tuned
2012-02-14 bulwahn 2012-02-14 adding abort_potential configuration in Quickcheck
2012-01-27 bulwahn 2012-01-27 adding some basic handling that unfolds a conjecture in a locale before testing it with quickcheck
2011-12-05 bulwahn 2011-12-05 making the default behaviour of quickcheck a little bit less verbose; adapting quickcheck examples
2011-12-05 bulwahn 2011-12-05 adding verbose configuration to quickcheck
2011-12-05 bulwahn 2011-12-05 renaming potential flag to genuine_only flag with an inverse semantics
2011-12-05 bulwahn 2011-12-05 outputing the potentially spurious counterexample and continue search
2011-12-01 bulwahn 2011-12-01 outputing if counterexample is potentially spurious or not
2011-12-01 bulwahn 2011-12-01 extending quickcheck's result by the genuine flag
2011-11-30 bulwahn 2011-11-30 adding parsing of potential configuration to quickcheck command
2011-11-30 bulwahn 2011-11-30 adding quickcheck's potential configuration
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-11-11 bulwahn 2011-11-11 adding option allow_function_inversion to quickcheck options