adding the predicate compiler quickcheck to the ex/ROOT.ML; adopting this quickcheck to the latest changes
authorbulwahn
Thu, 12 Nov 2009 20:39:02 +0100
changeset 33651 e4aad90618ad
parent 33650 dd3ea99d5c76
child 33652 d7836058f52b
adding the predicate compiler quickcheck to the ex/ROOT.ML; adopting this quickcheck to the latest changes
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/ex/ROOT.ML
--- 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 [