src/HOL/Library/Numeral_Type.thy
changeset 30729 461ee3e49ad3
parent 30663 0b6aff7451b2
child 30960 fec1a04b7220
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Thu Mar 26 19:24:21 2009 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Thu Mar 26 20:08:55 2009 +0100
     1.3 @@ -313,7 +313,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -interpretation bit0!:
     1.8 +interpretation bit0:
     1.9    mod_type "int CARD('a::finite bit0)"
    1.10             "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
    1.11             "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
    1.12 @@ -329,7 +329,7 @@
    1.13  apply (rule power_bit0_def [unfolded Abs_bit0'_def])
    1.14  done
    1.15  
    1.16 -interpretation bit1!:
    1.17 +interpretation bit1:
    1.18    mod_type "int CARD('a::finite bit1)"
    1.19             "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
    1.20             "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
    1.21 @@ -363,13 +363,13 @@
    1.22  
    1.23  end
    1.24  
    1.25 -interpretation bit0!:
    1.26 +interpretation bit0:
    1.27    mod_ring "int CARD('a::finite bit0)"
    1.28             "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
    1.29             "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
    1.30    ..
    1.31  
    1.32 -interpretation bit1!:
    1.33 +interpretation bit1:
    1.34    mod_ring "int CARD('a::finite bit1)"
    1.35             "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
    1.36             "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"