src/HOL/Mutabelle/mutabelle_extra.ML
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