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