src/HOL/Predicate_Compile.thy
2011-11-11 bulwahn 2011-11-11 adding CPS compilation to predicate compiler; removing function_flattening reference; new testers smart_exhaustive and smart_slow_exhaustive; renaming PredicateCompFuns to Predicate_Comp_Funs;
2010-10-21 bulwahn 2010-10-21 splitting large core file into core_data, mode_inference and predicate_compile_proof
2010-03-31 bulwahn 2010-03-31 putting compilation setup of predicate compiler in a separate file
2010-03-29 bulwahn 2010-03-29 adding specialisation of predicates to the predicate compiler
2010-03-29 bulwahn 2010-03-29 adopting Predicate_Compile
2010-03-22 wenzelm 2010-03-22 recovered header;
2010-03-22 bulwahn 2010-03-22 removed unused Predicate_Compile_Set
2010-03-22 bulwahn 2010-03-22 reviving the classical depth-limited computation in the predicate compiler
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-10-28 wenzelm 2009-10-28 proper headers;
2009-10-27 bulwahn 2009-10-27 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck