removed redundant instance declarations inat :: linorder
authorhuffman
Mon, 11 May 2009 08:24:35 -0700
changeset 31094 7d6edb28bdbc
parent 31086 3e69a25b90a2
child 31095 b79d140f6d0b
removed redundant instance declarations inat :: linorder
src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Mon May 11 15:05:17 2009 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy	Mon May 11 08:24:35 2009 -0700
@@ -268,9 +268,6 @@
 
 end
 
-instance inat :: linorder
-by intro_classes (auto simp add: less_eq_inat_def split: inat.splits)
-
 instance inat :: pordered_comm_semiring
 proof
   fix a b c :: inat
@@ -423,8 +420,4 @@
 
 lemmas inat_splits = inat.splits
 
-
-instance inat :: linorder
-by intro_classes (auto simp add: inat_defs split: inat.splits)
-
 end