--- a/src/HOL/Library/Numeral_Type.thy Fri Feb 20 09:15:23 2009 -0800
+++ b/src/HOL/Library/Numeral_Type.thy Fri Feb 20 11:58:00 2009 -0800
@@ -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