2010-05-19 bulwahn 2010-05-19 improved behaviour of defined_functions in the predicate compiler
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-29 haftmann 2010-04-29 dropped unnecessary ML code
2010-04-28 bulwahn 2010-04-28 removed local clone in the predicate compiler
2010-04-28 bulwahn 2010-04-28 improving proof procedure for transforming cases rule in the predicate compiler to handle free variables of function type
2010-04-25 wenzelm 2010-04-25 modernized naming conventions of main Isar proof elements;
2010-04-21 bulwahn 2010-04-21 make profiling depend on reference Quickcheck.timing
2010-04-21 bulwahn 2010-04-21 removing dead code; clarifying function names; removing clone
2010-04-21 bulwahn 2010-04-21 added switch detection to the predicate compiler
2010-04-21 bulwahn 2010-04-21 adding more profiling to the predicate compiler
2010-04-21 bulwahn 2010-04-21 only add relevant predicates to the list of extra modes
2010-04-21 bulwahn 2010-04-21 prefer functional modes of functions in the mode analysis
2010-03-31 bulwahn 2010-03-31 made smlnj happy
2010-03-31 bulwahn 2010-03-31 clarifying the Predicate_Compile_Core signature
2010-03-31 bulwahn 2010-03-31 putting compilation setup of predicate compiler in a separate file
2010-03-29 bulwahn 2010-03-29 generalized alternative functions to alternative compilation to handle arithmetic functions better
2010-03-29 bulwahn 2010-03-29 correcting alternative functions with tuples
2010-03-29 bulwahn 2010-03-29 adding registration of functions in the function flattening
2010-03-29 bulwahn 2010-03-29 added book-keeping, registration and compilation with alternative functions for predicates in the predicate compiler
2010-03-29 bulwahn 2010-03-29 returning an more understandable user error message in the values command
2010-03-29 bulwahn 2010-03-29 adding Lazy_Sequences with explicit depth-bound
2010-03-29 bulwahn 2010-03-29 prefer recursive calls before others in the mode inference
2010-03-29 bulwahn 2010-03-29 added statistics to values command for random generation
2010-03-29 bulwahn 2010-03-29 made quickcheck generic with respect to which compilation; added random compilation to quickcheck
2010-03-29 bulwahn 2010-03-29 adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
2010-03-29 bulwahn 2010-03-29 generalizing the compilation process of the predicate compiler
2010-03-29 bulwahn 2010-03-29 added new compilation to predicate_compiler
2010-03-28 wenzelm 2010-03-28 implicit checkpoint in Local_Theory.theory as well -- no longer export Local_Theory.checkpoint;
2010-03-22 bulwahn 2010-03-22 contextifying the compilation of the predicate compiler
2010-03-22 bulwahn 2010-03-22 avoiding fishing for split_asm rule in the predicate compiler
2010-03-22 bulwahn 2010-03-22 contextifying the proof procedure in the predicate compiler
2010-03-22 bulwahn 2010-03-22 making flat triples to nested tuple to remove general triple functions
2010-03-22 bulwahn 2010-03-22 reduced the debug output functions from 2 to 1
2010-03-22 bulwahn 2010-03-22 some improvements thanks to Makarius source code review
2010-03-22 bulwahn 2010-03-22 adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
2010-03-22 bulwahn 2010-03-22 adding depth_limited_random compilation to predicate compiler
2010-03-22 bulwahn 2010-03-22 a new simpler random compilation for the predicate compiler
2010-03-22 bulwahn 2010-03-22 reviving the classical depth-limited computation in the predicate compiler
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-01 bulwahn 2010-03-01 made smlnj happy
2010-02-27 wenzelm 2010-02-27 clarified @{const_name} vs. @{const_abbrev};
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-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2010-01-22 haftmann 2010-01-22 merged
2010-01-22 haftmann 2010-01-22 HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
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-12-07 haftmann 2009-12-07 split off evaluation mechanisms in separte module Code_Eval
2009-11-30 haftmann 2009-11-30 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-19 bulwahn 2009-11-19 adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
2009-11-19 bulwahn 2009-11-19 changing the proof procedure for parameters; adding a testcase for negation and parameters; adopting print_tac to the latest function print_tac' in the predicate compiler
2009-11-19 bulwahn 2009-11-19 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-12 bulwahn 2009-11-12 removed annoying tracing message
2009-11-12 bulwahn 2009-11-12 improving code quality thanks to Florian's code review
2009-11-12 bulwahn 2009-11-12 renaming code_pred_intros to code_pred_intro * * * adopted alternative definitions for the predicate compiler to new attribute name
2009-11-12 bulwahn 2009-11-12 new names for predicate functions in the predicate compiler * * * adopting examples of the predicate compiler
2009-11-12 bulwahn 2009-11-12 changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned