src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
2010-06-24 haftmann 2010-06-24 more precise tactic: do not escape to a different goal branch (REPEAT is still problematic, though)
2010-06-10 haftmann 2010-06-10 tuned quotes, antiquotations and whitespace
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-26 haftmann 2010-05-26 normalized references to constant "split"
2010-05-20 bulwahn 2010-05-20 deactivated timing of infering modes
2010-05-19 bulwahn 2010-05-19 changing operations for accessing data to work with contexts
2010-05-19 bulwahn 2010-05-19 removed unnecessary Thm.transfer in the predicate compiler
2010-05-19 bulwahn 2010-05-19 changing compilation to work only with contexts; adapting quickcheck
2010-05-19 bulwahn 2010-05-19 removing unused argument in print_modes function
2010-05-19 bulwahn 2010-05-19 moving towards working with proof contexts in the predicate compiler
2010-05-19 bulwahn 2010-05-19 improved values command to handle a special case with tuples and polymorphic predicates more correctly
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