1.1 --- a/src/HOL/Library/Numeral_Type.thy	Fri Feb 20 09:15:23 2009 -0800
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Fri Feb 20 11:58:00 2009 -0800
     1.3 @@ -267,6 +267,22 @@
     1.4  
     1.5  subsection {* Number ring instances *}
     1.6  
     1.7 +text {*
     1.8 +  Unfortunately a number ring instance is not possible for
     1.9 +  @{typ num1}, since 0 and 1 are not distinct.
    1.10 +*}
    1.11 +
    1.12 +instantiation num1 :: "{comm_ring,comm_monoid_mult,number,recpower}"
    1.13 +begin
    1.14 +
    1.15 +lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
    1.16 +  by (induct x, induct y) simp
    1.17 +
    1.18 +instance proof
    1.19 +qed (simp_all add: num1_eq_iff)
    1.20 +
    1.21 +end
    1.22 +
    1.23  instantiation
    1.24    bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus,power}"
    1.25  begin