# HG changeset patch
# User huffman
# Date 1235159880 28800
# Node ID c7f0c1b8001b608765bd7da883bf605e23b7f989
# Parent  80db6f3c523ef969c24179746371fa6e8e017200
class instances for num1

diff -r 80db6f3c523e -r c7f0c1b8001b src/HOL/Library/Numeral_Type.thy
--- 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