src/HOL/Quickcheck_Examples/Completeness.thy
changeset 58813 625d04d4fd2a
parent 57645 ee55e667dedc
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Quickcheck_Examples/Completeness.thy	Wed Oct 29 11:13:24 2014 +0100
     1.2 +++ b/src/HOL/Quickcheck_Examples/Completeness.thy	Wed Oct 29 11:19:27 2014 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4    "is_some x \<longleftrightarrow> x \<noteq> None"
     1.5    by (cases x) simp_all
     1.6  
     1.7 -setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *} 
     1.8 +setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
     1.9  
    1.10  subsection {* Defining the size of values *}
    1.11