# HG changeset patch
# User huffman
# Date 1179384083 -7200
# Node ID d21d3539f6bb7f51cba4ec70e5702407bedfd870
# Parent  501e6dfe4e5a51a4f7415c734cedc0821dfb31bb
remove redundant instance declaration

diff -r 501e6dfe4e5a -r d21d3539f6bb src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Thu May 17 00:45:27 2007 +0200
+++ b/src/HOL/OrderedGroup.thy	Thu May 17 08:41:23 2007 +0200
@@ -200,8 +200,6 @@
 class pordered_cancel_ab_semigroup_add =
   pordered_ab_semigroup_add + cancel_ab_semigroup_add
 
-instance pordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add ..
-
 class pordered_ab_semigroup_add_imp_le = pordered_cancel_ab_semigroup_add +
   assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b \<Longrightarrow> a \<sqsubseteq> b"