src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
changeset 40924 a9be7f26b4e6
parent 39800 17e29ddd538e
child 41956 c15ef1b85035
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Fri Dec 03 08:40:47 2010 +0100
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Fri Dec 03 08:40:47 2010 +0100
     1.3 @@ -92,7 +92,7 @@
     1.4  
     1.5  lemma
     1.6    "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
     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  text {* Verifying that the found counterexample really is one by means of a proof *}