src/HOL/Enum.thy

 
 subsection {* Small finite types *}
 
 text {* We define small finite types for use in Quickcheck *}
 
-datatype (plugins only: code "quickcheck*") finite_1 = a\<^sub>1
+datatype (plugins only: code "quickcheck*" extraction) finite_1 =
+  a\<^sub>1
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
 
 lemma UNIV_finite_1:
   "UNIV = {a\<^sub>1}"

 end
 
 declare [[simproc del: finite_1_eq]]
 hide_const (open) a\<^sub>1
 
-datatype (plugins only: code "quickcheck*") finite_2 = a\<^sub>1 | a\<^sub>2
+datatype (plugins only: code "quickcheck*" extraction) finite_2 =
+  a\<^sub>1 | a\<^sub>2
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
 notation (output) a\<^sub>2  ("a\<^sub>2")
 
 lemma UNIV_finite_2:

      split: finite_2.splits)
 end
 
 hide_const (open) a\<^sub>1 a\<^sub>2
 
-datatype (plugins only: code "quickcheck*") finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
+datatype (plugins only: code "quickcheck*" extraction) finite_3 =
+  a\<^sub>1 | a\<^sub>2 | a\<^sub>3
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
 notation (output) a\<^sub>2  ("a\<^sub>2")
 notation (output) a\<^sub>3  ("a\<^sub>3")
 

      split: finite_3.splits)
 end
 
 hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
 
-datatype (plugins only: code "quickcheck*") finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
+datatype (plugins only: code "quickcheck*" extraction) finite_4 =
+  a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
 notation (output) a\<^sub>2  ("a\<^sub>2")
 notation (output) a\<^sub>3  ("a\<^sub>3")
 notation (output) a\<^sub>4  ("a\<^sub>4")

   (simp_all add: inf_finite_4_def sup_finite_4_def uminus_finite_4_def minus_finite_4_def split: finite_4.splits)
 end
 
 hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
 
-datatype (plugins only: code "quickcheck*") finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
+datatype (plugins only: code "quickcheck*" extraction) finite_5 =
+  a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
 notation (output) a\<^sub>2  ("a\<^sub>2")
 notation (output) a\<^sub>3  ("a\<^sub>3")
 notation (output) a\<^sub>4  ("a\<^sub>4")