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