src/HOL/Enum.thy
changeset 58659 6c9821c32dd5
parent 58646 cd63a4b12a33
child 58710 7216a10d69ba
     1.1 --- a/src/HOL/Enum.thy	Mon Oct 13 17:04:25 2014 +0200
     1.2 +++ b/src/HOL/Enum.thy	Mon Oct 13 18:45:48 2014 +0200
     1.3 @@ -493,7 +493,7 @@
     1.4  
     1.5  text {* We define small finite types for use in Quickcheck *}
     1.6  
     1.7 -datatype (plugins only: code "quickcheck*" extraction) finite_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 @@ -596,7 +596,7 @@
    1.13  declare [[simproc del: finite_1_eq]]
    1.14  hide_const (open) a\<^sub>1
    1.15  
    1.16 -datatype (plugins only: code "quickcheck*" extraction) finite_2 =
    1.17 +datatype (plugins only: code "quickcheck" extraction) finite_2 =
    1.18    a\<^sub>1 | a\<^sub>2
    1.19  
    1.20  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.21 @@ -711,7 +711,7 @@
    1.22  
    1.23  hide_const (open) a\<^sub>1 a\<^sub>2
    1.24  
    1.25 -datatype (plugins only: code "quickcheck*" extraction) finite_3 =
    1.26 +datatype (plugins only: code "quickcheck" extraction) finite_3 =
    1.27    a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    1.28  
    1.29  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.30 @@ -838,7 +838,7 @@
    1.31  
    1.32  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
    1.33  
    1.34 -datatype (plugins only: code "quickcheck*" extraction) finite_4 =
    1.35 +datatype (plugins only: code "quickcheck" extraction) finite_4 =
    1.36    a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
    1.37  
    1.38  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.39 @@ -940,7 +940,7 @@
    1.40  
    1.41  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
    1.42  
    1.43 -datatype (plugins only: code "quickcheck*" extraction) finite_5 =
    1.44 +datatype (plugins only: code "quickcheck" extraction) finite_5 =
    1.45    a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
    1.46  
    1.47  notation (output) a\<^sub>1  ("a\<^sub>1")