src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
changeset 40924 a9be7f26b4e6
parent 40301 bf39a257b3d3
child 41956 c15ef1b85035
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Fri Dec 03 08:40:47 2010 +0100
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Fri Dec 03 08:40:47 2010 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4  
     1.5  lemma
     1.6    "w \<in> S\<^isub>1 \<Longrightarrow> w = []"
     1.7 -quickcheck[generator = prolog, iterations=1, expect = counterexample]
     1.8 +quickcheck[tester = prolog, iterations=1, expect = counterexample]
     1.9  oops
    1.10  
    1.11  definition "filter_a = filter (\<lambda>x. x = a)"
    1.12 @@ -67,7 +67,7 @@
    1.13  
    1.14  theorem S\<^isub>1_sound:
    1.15  "w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.16 -quickcheck[generator = prolog, iterations=1, expect = counterexample]
    1.17 +quickcheck[tester = prolog, iterations=1, expect = counterexample]
    1.18  oops
    1.19  
    1.20  
    1.21 @@ -91,7 +91,7 @@
    1.22  
    1.23  theorem S\<^isub>2_sound:
    1.24  "w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.25 -quickcheck[generator=prolog, iterations=1, expect = counterexample]
    1.26 +quickcheck[tester = prolog, iterations=1, expect = counterexample]
    1.27  oops
    1.28  
    1.29  inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
    1.30 @@ -113,7 +113,7 @@
    1.31  
    1.32  lemma S\<^isub>3_sound:
    1.33  "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.34 -quickcheck[generator=prolog, iterations=1, size=1, expect = no_counterexample]
    1.35 +quickcheck[tester = prolog, iterations=1, size=1, expect = no_counterexample]
    1.36  oops
    1.37  
    1.38  
    1.39 @@ -131,7 +131,7 @@
    1.40  
    1.41  theorem S\<^isub>3_complete:
    1.42  "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
    1.43 -quickcheck[generator = prolog, size=1, iterations=1]
    1.44 +quickcheck[tester = prolog, size=1, iterations=1]
    1.45  oops
    1.46  *)
    1.47  
    1.48 @@ -156,7 +156,7 @@
    1.49  
    1.50  theorem S\<^isub>4_sound:
    1.51  "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.52 -quickcheck[generator = prolog, size=1, iterations=1, expect = no_counterexample]
    1.53 +quickcheck[tester = prolog, size=1, iterations=1, expect = no_counterexample]
    1.54  oops
    1.55  
    1.56  (*