src/HOL/Library/Numeral_Type.thy
changeset 49834 b27bbb021df1
parent 48063 f02b4302d5dd
child 51153 b14ee572cc7b
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Fri Oct 12 15:08:29 2012 +0200
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Fri Oct 12 18:58:20 2012 +0200
     1.3 @@ -10,16 +10,16 @@
     1.4  
     1.5  subsection {* Numeral Types *}
     1.6  
     1.7 -typedef (open) num0 = "UNIV :: nat set" ..
     1.8 -typedef (open) num1 = "UNIV :: unit set" ..
     1.9 +typedef num0 = "UNIV :: nat set" ..
    1.10 +typedef num1 = "UNIV :: unit set" ..
    1.11  
    1.12 -typedef (open) 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}"
    1.13 +typedef 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}"
    1.14  proof
    1.15    show "0 \<in> {0 ..< 2 * int CARD('a)}"
    1.16      by simp
    1.17  qed
    1.18  
    1.19 -typedef (open) 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}"
    1.20 +typedef 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}"
    1.21  proof
    1.22    show "0 \<in> {0 ..< 1 + 2 * int CARD('a)}"
    1.23      by simp