src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
changeset 36040 fcd7bea01a93
parent 35955 e657fb805c68
child 36176 3fe7e97ccca8
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Mon Mar 29 17:30:55 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Mon Mar 29 17:30:56 2010 +0200
     1.3 @@ -108,7 +108,7 @@
     1.4  | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
     1.5  | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
     1.6  
     1.7 -code_pred [inductify] S\<^isub>3 .
     1.8 +code_pred [inductify, skip_proof] S\<^isub>3 .
     1.9  thm S\<^isub>3.equation
    1.10  (*
    1.11  values 10 "{x. S\<^isub>3 x}"