# HG changeset patch
# User huffman
# Date 1234818876 28800
# Node ID ca43d393c2f1f396c887e7acc1a47b5ac20fe0e8
# Parent  922b931fd2ebe73856389f04acc7cb0c82b45098
remove instances num::semiring and num::linorder

diff -r 922b931fd2eb -r ca43d393c2f1 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Mon Feb 16 13:08:21 2009 -0800
+++ b/src/HOL/ex/Numeral.thy	Mon Feb 16 13:14:36 2009 -0800
@@ -67,7 +67,7 @@
   apply (simp add: nat_of_num_inverse)
   done
 
-instantiation num :: "semiring"
+instantiation num :: "{plus,times}"
 begin
 
 definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where
@@ -84,8 +84,7 @@
   unfolding times_num_def
   by (intro num_of_nat_inverse mult_pos_pos nat_of_num_gt_0)
 
-instance proof
-qed (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult nat_distrib)
+instance ..
 
 end
 
@@ -389,7 +388,7 @@
   ultimately show ?thesis by (simp add: of_nat_of_num)
 qed
 
-instantiation num :: linorder
+instantiation num :: ord
 begin
 
 definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
@@ -398,8 +397,7 @@
 definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
   [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
 
-instance proof
-qed (auto simp add: less_eq_num_def less_num_def num_eq_iff)
+instance ..
 
 end
 
@@ -487,8 +485,11 @@
 lemma DigM_plus_one: "DigM n + One = Dig0 n"
   by (induct n) simp_all
 
+lemma add_One_commute: "One + n = n + One"
+  by (induct n) simp_all
+
 lemma one_plus_DigM: "One + DigM n = Dig0 n"
-  unfolding add_commute [of One] DigM_plus_one ..
+  unfolding add_One_commute DigM_plus_one ..
 
 class semiring_minus = semiring + minus + zero +
   assumes minus_inverts_plus1: "a + b = c \<Longrightarrow> c - b = a"