2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-25 bulwahn 2010-08-25 invocation of values for prolog execution does not require invocation of code_pred anymore
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-05-19 bulwahn 2010-05-19 changing operations for accessing data to work with contexts
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-12 bulwahn 2010-03-12 adopting predicate compiler to changes in Spec_Rules; removed dependency to Nitpick_Intros
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2010-02-27 wenzelm 2010-02-27 code simplification by inlining;
2010-02-27 wenzelm 2010-02-27 just one copy of structure Term_Graph (in Pure);
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-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
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-21 bulwahn 2010-01-21 adopting predicate compiler to new Spec_Rules and eliminating the use of Nitpick_Simps
2010-01-20 bulwahn 2010-01-20 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
2009-11-19 bulwahn 2009-11-19 replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
2009-11-12 bulwahn 2009-11-12 adding more tests for the values command; adding some forbidden constants to inductify * * * added further testcase for values command
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-06 bulwahn 2009-11-06 merged
2009-11-06 bulwahn 2009-11-06 made SML/NJ happy; tuned
2009-11-05 wenzelm 2009-11-05 eliminated funny record patterns and made SML/NJ happy;
2009-11-03 bulwahn 2009-11-03 adapted the inlining in the predicate compiler
2009-10-31 bulwahn 2009-10-31 predicate compiler creates code equations for predicates with full mode
2009-10-28 wenzelm 2009-10-28 proper headers;
2009-10-27 bulwahn 2009-10-27 print retrieved specification when printing intermediate results
2009-10-27 bulwahn 2009-10-27 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck