--- a/src/HOL/Library/Numeral_Type.thy Sat Feb 21 09:58:26 2009 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Sat Feb 21 09:58:45 2009 +0100
@@ -267,6 +267,22 @@
subsection {* Number ring instances *}
+text {*
+ Unfortunately a number ring instance is not possible for
+ @{typ num1}, since 0 and 1 are not distinct.
+*}
+
+instantiation num1 :: "{comm_ring,comm_monoid_mult,number,recpower}"
+begin
+
+lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
+ by (induct x, induct y) simp
+
+instance proof
+qed (simp_all add: num1_eq_iff)
+
+end
+
instantiation
bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus,power}"
begin