src/HOL/Predicate_Compile.thy
2016-07-11 wenzelm 2016-07-11 tuned;
2016-02-23 nipkow 2016-02-23 more canonical names
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-02-17 wenzelm 2014-02-17 more informative error;
2013-05-16 Andreas Lochbihler 2013-05-16 setup for set membership as a predicate for code_pred
2013-02-14 haftmann 2013-02-14 reform of predicate compiler / quickcheck theories: implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers! avoid odd New_ prefix by joining related theories; avoid overcompact name DSequence; separated predicate inside random monad into separate theory; consolidated name of theory Quickcheck
2012-11-12 haftmann 2012-11-12 tuned import order
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-02-24 haftmann 2012-02-24 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24 haftmann 2012-02-24 given up disfruitful branch
2012-02-23 haftmann 2012-02-23 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
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