# HG changeset patch
# User bulwahn
# Date 1311142602 -7200
# Node ID eabe4d6fbd131b2fcc7ad7915e138a0670f20a65
# Parent  ef347714c5c119a9666f4ffba704183c29bed31d
deactivating quickcheck invocation in this example until the Interrupt issue is understood

diff -r ef347714c5c1 -r eabe4d6fbd13 src/HOL/Predicate_Compile_Examples/ROOT.ML
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Wed Jul 20 08:16:41 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Wed Jul 20 08:16:42 2011 +0200
@@ -3,7 +3,7 @@
   "Predicate_Compile_Tests",
 (*  "Predicate_Compile_Quickcheck_Examples", -- should be added again soon *)
   "Specialisation_Examples",
-  "Hotel_Example_Small_Generator",
+(*  "Hotel_Example_Small_Generator",*)
   "IMP_1",
   "IMP_2"
 (*  "IMP_3",