# HG changeset patch
# User haftmann
# Date 1207144708 -7200
# Node ID 294708d83e83e112e49be8a2b6a533de7dd3ad7e
# Parent  4cd7c4f936bb1314de3d7cd7ce23e27ce8d2b0b9
dropped wrong code lemma

diff -r 4cd7c4f936bb -r 294708d83e83 src/HOL/Library/Abstract_Rat.thy
--- a/src/HOL/Library/Abstract_Rat.thy	Wed Apr 02 15:58:27 2008 +0200
+++ b/src/HOL/Library/Abstract_Rat.thy	Wed Apr 02 15:58:28 2008 +0200
@@ -264,7 +264,7 @@
   ultimately show ?thesis by blast
 qed
 
-lemma INum_normNum_iff [code]: "(INum x ::'a::{field, division_by_zero, ring_char_0}) = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
+lemma INum_normNum_iff: "(INum x ::'a::{field, division_by_zero, ring_char_0}) = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
 proof -
   have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
     by (simp del: normNum)