src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
2009-11-13 wenzelm 2009-11-13 inductive: eliminated obsolete kind;
2009-11-12 wenzelm 2009-11-12 eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-12 bulwahn 2009-11-12 removed unnecessary oracle in the predicate compiler
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-28 wenzelm 2009-10-28 conceal internal bindings;
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