src/HOL/Mutabelle/mutabelle_extra.ML
2015-04-06 wenzelm 2015-04-06 local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-01-24 wenzelm 2015-01-24 tuned signature;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete Output.urgent_message;
2014-09-01 blanchet 2014-09-01 tuned structure inclusion
2014-04-08 wenzelm 2014-04-08 more uniform ML/document antiquotations;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-15 wenzelm 2014-03-15 tuned signature; eliminated clones;
2014-03-14 wenzelm 2014-03-14 prefer more robust Synchronized.var;
2014-01-31 blanchet 2014-01-31 tuned ML file name
2013-07-13 wenzelm 2013-07-13 compile
2013-07-12 wenzelm 2013-07-12 system options for Isabelle/HOL proof tools;
2013-02-15 haftmann 2013-02-15 systematic conversions between nat and nibble/char; more uniform approaches to execute operations on nibble/char
2013-02-14 haftmann 2013-02-14 reform of predicate compiler / quickcheck theories: implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers! avoid odd New_ prefix by joining related theories; avoid overcompact name DSequence; separated predicate inside random monad into separate theory; consolidated name of theory Quickcheck
2013-02-13 haftmann 2013-02-13 formal cleanup of sources
2012-09-19 bulwahn 2012-09-19 recording elapsed time in mutabelle for more detailed evaluation
2012-04-24 blanchet 2012-04-24 handle TPTP definitions as definitions in Nitpick rather than as axioms
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-02-27 wenzelm 2012-02-27 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
2012-02-24 blanchet 2012-02-24 renamed 'try_methods' to 'try0'
2012-02-11 bulwahn 2012-02-11 making num_mutations a configuration that can be changed with the mutabelle bash command
2012-02-11 bulwahn 2012-02-11 making max_mutants an option that can be changed in the Mutabelle-script
2012-02-11 bulwahn 2012-02-11 increase timeout to 30 seconds; changing mutabelle script
2012-02-05 bulwahn 2012-02-05 adding some forbidden constant names for mutabelle
2012-02-05 bulwahn 2012-02-05 mutabelle ignores theorems with internal constants
2012-01-31 bulwahn 2012-01-31 mutabelle must handle the case where quickcheck returns multiple results
2012-01-24 bulwahn 2012-01-24 some more constants on mutabelle's blacklist
2012-01-23 bulwahn 2012-01-23 adding another internal constant to mutabelle's blacklust
2012-01-23 bulwahn 2012-01-23 adding some more forbidden constant names for the mutated conjecture generation
2012-01-23 bulwahn 2012-01-23 more configurations to mutabelle
2011-11-09 bulwahn 2011-11-09 quickcheck invocations in mutabelle must not catch codegenerator errors internally
2011-11-07 blanchet 2011-11-07 revived Refute in Mutabelle
2011-10-18 bulwahn 2011-10-18 adding testing of quickcheck narrowing with finite types to mutabelle script; modified is_executable in mutabelle_extra
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-08-08 huffman 2011-08-08 moved division ring stuff from Rings.thy to Fields.thy
2011-07-18 bulwahn 2011-07-18 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
2011-06-08 wenzelm 2011-06-08 pervasive Output operations;
2011-06-07 bulwahn 2011-06-07 printing environment in mutabelle's log
2011-05-31 blanchet 2011-05-31 compile
2011-05-27 blanchet 2011-05-27 compile
2011-05-27 blanchet 2011-05-27 renamed "Auto_Tools" "Try"
2011-04-20 wenzelm 2011-04-20 merged;
2011-04-20 bulwahn 2011-04-20 adding two further code-generator internal constants to the blacklist of Mutabelle
2011-04-20 wenzelm 2011-04-20 standardized some ML aliases;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-31 blanchet 2011-03-31 added support for "dest:" to "try"
2011-03-23 bulwahn 2011-03-23 adapting mutabelle; exporting more Quickcheck functions
2011-03-21 bulwahn 2011-03-21 merged
2011-03-18 bulwahn 2011-03-18 adapting mutabelle
2011-03-20 wenzelm 2011-03-20 simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
2011-03-20 wenzelm 2011-03-20 structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;
2011-03-18 blanchet 2011-03-18 added "simp:", "intro:", and "elim:" to "try" command
2011-02-11 bulwahn 2011-02-11 adjusting HOL-Mutabelle to changes in quickcheck
2011-01-10 wenzelm 2011-01-10 eliminated Int.toString;
2010-12-29 wenzelm 2010-12-29 made SML/NJ happy;
2010-12-29 wenzelm 2010-12-29 tuned comments;