# HG changeset patch
# User huffman
# Date 1242055475 25200
# Node ID 7d6edb28bdbc149af5f91b997f068a41501a392f
# Parent  3e69a25b90a238452f9838725378fa68f95fc825
removed redundant instance declarations inat :: linorder

diff -r 3e69a25b90a2 -r 7d6edb28bdbc 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