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
2011-11-09 bulwahn 2011-11-09 quickcheck fails with code generator errors only if one tester is invoked
2011-11-09 bulwahn 2011-11-09 removing extra arguments
2011-10-31 bulwahn 2011-10-31 tuned
2011-10-20 bulwahn 2011-10-20 adding depth as an quickcheck configuration
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-07-20 bulwahn 2011-07-20 removing inner time limits in quickcheck
2011-07-20 bulwahn 2011-07-20 exporting function in quickcheck; adapting mutabelle script
2011-07-18 bulwahn 2011-07-18 quickcheck does not deactivate testers if none are given
2011-07-18 bulwahn 2011-07-18 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
2011-07-18 bulwahn 2011-07-18 renaming quickcheck_tester to quickcheck_batch_tester; tuned
2011-07-18 bulwahn 2011-07-18 changing parser in quickcheck to activate and deactivate the testers
2011-07-18 bulwahn 2011-07-18 enabling parallel execution of testers but removing more informative quickcheck output
2011-07-18 bulwahn 2011-07-18 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
2011-07-18 bulwahn 2011-07-18 removing generator registration
2011-07-18 bulwahn 2011-07-18 parametrized test_term functions in quickcheck