diff -r cd6558ed65d7 -r d183bf90dabd src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Tue Sep 07 11:51:53 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Tue Sep 07 11:51:53 2010 +0200 @@ -1,4 +1,4 @@ -theory RegExp_Example +theory Reg_Exp_Example imports Predicate_Compile_Quickcheck Code_Prolog begin @@ -158,7 +158,7 @@ assumes "q = Seq (Sym N0) (Sym N0)" assumes "s = [N0, N0]" shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s" -quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample] +(*quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*) quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample] oops