src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 wenzelm 2010-08-27 merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 wenzelm 2010-08-26 simplification/standardization of some theory data;
2010-08-26 wenzelm 2010-08-26 renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
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-07-29 bulwahn 2010-07-29 exporting retrieval function for graph of introduction rules in the predicate compiler core
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-28 haftmann 2010-06-28 merged constants "split" and "prod_case"
2010-06-25 haftmann 2010-06-25 avoid REPEAT after THEN_ALL_NEW
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