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