src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy

 | "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
 | "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
 
 lemma
   "w \<in> S\<^isub>1 \<Longrightarrow> w = []"
-quickcheck[generator = prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1, expect = counterexample]
 oops
 
 definition "filter_a = filter (\<lambda>x. x = a)"
 
 lemma [code_pred_def]: "filter_a [] = []"

   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
 
 
 theorem S\<^isub>1_sound:
 "w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator = prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1, expect = counterexample]
 oops
 
 
 inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
   "[] \<in> S\<^isub>2"

   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
 
 
 theorem S\<^isub>2_sound:
 "w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1, expect = counterexample]
 oops
 
 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
   "[] \<in> S\<^isub>3"
 | "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"

   replacing = [(("s3", "limited_s3"), "quickcheck")],
   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
 
 lemma S\<^isub>3_sound:
 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=prolog, iterations=1, size=1, expect = no_counterexample]
+quickcheck[tester = prolog, iterations=1, size=1, expect = no_counterexample]
 oops
 
 
 (*
 setup {* Code_Prolog.map_code_options (K

   prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 
 theorem S\<^isub>3_complete:
 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
-quickcheck[generator = prolog, size=1, iterations=1]
+quickcheck[tester = prolog, size=1, iterations=1]
 oops
 *)
 
 inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
   "[] \<in> S\<^isub>4"

   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
 
 
 theorem S\<^isub>4_sound:
 "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator = prolog, size=1, iterations=1, expect = no_counterexample]
+quickcheck[tester = prolog, size=1, iterations=1, expect = no_counterexample]
 oops
 
 (*
 theorem S\<^isub>4_complete:
 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"