src/HOL/Enum.thy
changeset 58334 7553a1bcecb7
parent 58310 91ea607a34d8
child 58350 919149921e46
     1.1 --- a/src/HOL/Enum.thy	Sat Sep 13 18:08:45 2014 +0200
     1.2 +++ b/src/HOL/Enum.thy	Sun Sep 14 22:59:30 2014 +0200
     1.3 @@ -491,9 +491,9 @@
     1.4  
     1.5  subsection {* Small finite types *}
     1.6  
     1.7 -text {* We define small finite types for the use in Quickcheck *}
     1.8 +text {* We define small finite types for use in Quickcheck *}
     1.9  
    1.10 -datatype finite_1 = a\<^sub>1
    1.11 +datatype (plugins only: code "quickcheck*") finite_1 = a\<^sub>1
    1.12  
    1.13  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.14  
    1.15 @@ -595,7 +595,7 @@
    1.16  declare [[simproc del: finite_1_eq]]
    1.17  hide_const (open) a\<^sub>1
    1.18  
    1.19 -datatype finite_2 = a\<^sub>1 | a\<^sub>2
    1.20 +datatype (plugins only: code "quickcheck*") finite_2 = a\<^sub>1 | a\<^sub>2
    1.21  
    1.22  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.23  notation (output) a\<^sub>2  ("a\<^sub>2")
    1.24 @@ -701,7 +701,7 @@
    1.25  
    1.26  hide_const (open) a\<^sub>1 a\<^sub>2
    1.27  
    1.28 -datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    1.29 +datatype (plugins only: code "quickcheck*") finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    1.30  
    1.31  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.32  notation (output) a\<^sub>2  ("a\<^sub>2")
    1.33 @@ -825,7 +825,7 @@
    1.34  
    1.35  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
    1.36  
    1.37 -datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
    1.38 +datatype (plugins only: code "quickcheck*") finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
    1.39  
    1.40  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.41  notation (output) a\<^sub>2  ("a\<^sub>2")
    1.42 @@ -926,8 +926,7 @@
    1.43  
    1.44  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
    1.45  
    1.46 -
    1.47 -datatype finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
    1.48 +datatype (plugins only: code "quickcheck*") finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
    1.49  
    1.50  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.51  notation (output) a\<^sub>2  ("a\<^sub>2")