adding the predicate compiler quickcheck to the ex/ROOT.ML; adopting this quickcheck to the latest changes
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Nov 12 20:38:59 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Nov 12 20:39:02 2009 +0100
@@ -23,6 +23,8 @@
val options = Options {
expected_modes = NONE,
+ proposed_modes = [],
+ proposed_names = [],
show_steps = true,
show_intermediate_results = true,
show_proof_trace = false,
--- a/src/HOL/ex/ROOT.ML Thu Nov 12 20:38:59 2009 +0100
+++ b/src/HOL/ex/ROOT.ML Thu Nov 12 20:39:02 2009 +0100
@@ -13,7 +13,8 @@
"Codegenerator_Pretty_Test",
"NormalForm",
"Predicate_Compile",
- "Predicate_Compile_ex"
+ "Predicate_Compile_ex",
+ "Predicate_Compile_Quickcheck"
];
use_thys [