# HG changeset patch
# User huffman
# Date 1235174840 28800
# Node ID e54d4d41fe8f0f7aec35fb00e55bdcbcb9fb8db0
# Parent  c7f0c1b8001b608765bd7da883bf605e23b7f989# Parent  bd786c37af84da6df4795e1e9cb9b1b1679ed081
merged

diff -r bd786c37af84 -r e54d4d41fe8f src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Fri Feb 20 23:46:03 2009 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Fri Feb 20 16:07:20 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