Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lower expectation in Reg exp example
authorbulwahn
Tue, 07 Sep 2010 11:51:53 +0200
changeset 39196 6ceb8d38bc9e
parent 39195 5ab54bf226ac
child 39197 35fcab3da1b7
lower expectation in Reg exp example
src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy file | annotate | diff | comparison | revisions 
--- 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
@@ -169,13 +169,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, expect = counterexample]
+quickcheck[generator = predicate_compile_wo_ff]
 quickcheck[generator = prolog, expect = counterexample]
 oops
 
 lemma "prop_regex a_sol"
 quickcheck[generator = code, expect = counterexample]
-quickcheck[generator = predicate_compile_ff_fs, expect = counterexample]
+quickcheck[generator = predicate_compile_ff_fs]
 oops
 
 value [code] "prop_regex a_sol"
isabelle