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  (*
```