Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
changeset 40924 a9be7f26b4e6
parent 39800 17e29ddd538e
child 41413 64cd30d6b0b8 
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -89,9 +89,9 @@
 
 lemma "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
 (*nitpick
-quickcheck[generator = code, iterations = 10000]
-quickcheck[generator = predicate_compile_wo_ff]
-quickcheck[generator = predicate_compile_ff_fs]
+quickcheck[tester = random, iterations = 10000]
+quickcheck[tester = predicate_compile_wo_ff]
+quickcheck[tester = predicate_compile_ff_fs]
 oops*)
 oops
 
@@ -115,10 +115,10 @@
  prolog-style generation. *}
 
 lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
-quickcheck[generator = code, iterations = 100000, expect = counterexample]
-(*quickcheck[generator = predicate_compile_wo_ff]*)
-(*quickcheck[generator = predicate_compile_ff_fs, iterations = 1]*)
-(*quickcheck[generator = prolog, iterations = 1, size = 1]*)
+quickcheck[tester = random, iterations = 100000, expect = counterexample]
+(*quickcheck[tester = predicate_compile_wo_ff]*)
+(*quickcheck[tester = predicate_compile_ff_fs, iterations = 1]*)
+(*quickcheck[tester = prolog, iterations = 1, size = 1]*)
 oops
 
 section {* Given a partial solution *}
@@ -130,8 +130,8 @@
   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]*)
-quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample]
+(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1]*)
+quickcheck[tester = prolog, iterations = 1, size = 1, expect = counterexample]
 oops
 
 section {* Checking the counterexample *}
@@ -147,7 +147,7 @@
   assumes "q = Seq (Sym N0) (Sym N0)"
   assumes "s = [N0, N0]"
   shows "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
-(*quickcheck[generator = predicate_compile_wo_ff]*)
+(*quickcheck[tester = predicate_compile_wo_ff]*)
 oops
 
 lemma
@@ -157,8 +157,8 @@
   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 = prolog, iterations = 1, size = 1, expect = counterexample]
+(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*)
+quickcheck[tester = prolog, iterations = 1, size = 1, expect = counterexample]
 oops
 
 lemma
@@ -168,13 +168,13 @@
   assumes "q = Seq (Sym N0) (Sym N0)"
   assumes "s = [N0, N0]"
 shows "prop_regex (n, (k, (p, (q, s))))"
-quickcheck[generator = predicate_compile_wo_ff]
-quickcheck[generator = prolog, expect = counterexample]
+quickcheck[tester = predicate_compile_wo_ff]
+quickcheck[tester = prolog, expect = counterexample]
 oops
 
 lemma "prop_regex a_sol"
-quickcheck[generator = code, expect = counterexample]
-quickcheck[generator = predicate_compile_ff_fs]
+quickcheck[tester = random, expect = counterexample]
+quickcheck[tester = predicate_compile_ff_fs]
 oops
 
 value [code] "prop_regex a_sol"
isabelle