src/HOL/Mutabelle/mutabelle_extra.ML
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;
2010-12-16 bulwahn 2010-12-16 reactivating nitpick in Mutabelle
2010-12-10 bulwahn 2010-12-10 setting finite_type_size to 1 in mutabelle_extra
2010-12-06 bulwahn 2010-12-06 commenting out sledgehammer_mtd in Mutabelle
2010-12-06 bulwahn 2010-12-06 adding timeout to try invocation in mutabelle
2010-12-06 bulwahn 2010-12-06 adding filtering, sytactic welltyping, and sledgehammer method in mutabelle
2010-12-03 blanchet 2010-12-03 compile
2010-12-03 blanchet 2010-12-03 run synchronous Auto Tools in parallel
2010-12-03 bulwahn 2010-12-03 adapting mutabelle
2010-12-03 bulwahn 2010-12-03 adapting mutabelle
2010-11-22 bulwahn 2010-11-22 adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
2010-11-05 wenzelm 2010-11-05 explicit indication of some remaining violations of the Isabelle/ML interrupt model;
2010-11-02 wenzelm 2010-11-02 simplified some time constants;
2010-10-29 bulwahn 2010-10-29 adapting HOL-Mutabelle to changes in quickcheck
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-09-20 wenzelm 2010-09-20 added XML.content_of convenience -- cover XML.body, which is the general situation;
2010-09-11 blanchet 2010-09-11 finished renaming "Auto_Counterexample" to "Auto_Tools"
2010-09-09 bulwahn 2010-09-09 removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
2010-09-05 wenzelm 2010-09-05 pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-07-08 haftmann 2010-07-08 tuned titles
2010-05-08 wenzelm 2010-05-08 prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-21 bulwahn 2010-04-21 tuning mutabelle; adding output of mutant theoryfile for interactive evaluation
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-02 bulwahn 2010-03-02 adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck
2010-02-25 bulwahn 2010-02-25 adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
2010-02-23 bulwahn 2010-02-23 adding ROOT.ML to HOL-Mutabelle session; uncommenting HOL.induct constants in Mutabelle session
2010-02-23 bulwahn 2010-02-23 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2010-01-25 bulwahn 2010-01-25 adding Mutabelle to repository