src/HOL/Enum.thy
changeset 58350 919149921e46
parent 58334 7553a1bcecb7
child 58646 cd63a4b12a33
     1.1 --- a/src/HOL/Enum.thy	Tue Sep 16 18:42:33 2014 +0200
     1.2 +++ b/src/HOL/Enum.thy	Tue Sep 16 19:23:37 2014 +0200
     1.3 @@ -493,7 +493,8 @@
     1.4  
     1.5  text {* We define small finite types for use in Quickcheck *}
     1.6  
     1.7 -datatype (plugins only: code "quickcheck*") finite_1 = a\<^sub>1
     1.8 +datatype (plugins only: code "quickcheck*" extraction) finite_1 =
     1.9 +  a\<^sub>1
    1.10  
    1.11  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.12  
    1.13 @@ -595,7 +596,8 @@
    1.14  declare [[simproc del: finite_1_eq]]
    1.15  hide_const (open) a\<^sub>1
    1.16  
    1.17 -datatype (plugins only: code "quickcheck*") finite_2 = a\<^sub>1 | a\<^sub>2
    1.18 +datatype (plugins only: code "quickcheck*" extraction) finite_2 =
    1.19 +  a\<^sub>1 | a\<^sub>2
    1.20  
    1.21  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.22  notation (output) a\<^sub>2  ("a\<^sub>2")
    1.23 @@ -701,7 +703,8 @@
    1.24  
    1.25  hide_const (open) a\<^sub>1 a\<^sub>2
    1.26  
    1.27 -datatype (plugins only: code "quickcheck*") finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    1.28 +datatype (plugins only: code "quickcheck*" extraction) finite_3 =
    1.29 +  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 +828,8 @@
    1.34  
    1.35  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
    1.36  
    1.37 -datatype (plugins only: code "quickcheck*") finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
    1.38 +datatype (plugins only: code "quickcheck*" extraction) finite_4 =
    1.39 +  a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
    1.40  
    1.41  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.42  notation (output) a\<^sub>2  ("a\<^sub>2")
    1.43 @@ -926,7 +930,8 @@
    1.44  
    1.45  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
    1.46  
    1.47 -datatype (plugins only: code "quickcheck*") finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
    1.48 +datatype (plugins only: code "quickcheck*" extraction) finite_5 =
    1.49 +  a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
    1.50  
    1.51  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.52  notation (output) a\<^sub>2  ("a\<^sub>2")