dropped wrong code lemma
authorhaftmann
Wed Apr 02 15:58:28 2008 +0200 (2008-04-02)
changeset 26509294708d83e83
parent 26508 4cd7c4f936bb
child 26510 a329af578d69
dropped wrong code lemma
src/HOL/Library/Abstract_Rat.thy
     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Wed Apr 02 15:58:27 2008 +0200
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Wed Apr 02 15:58:28 2008 +0200
     1.3 @@ -264,7 +264,7 @@
     1.4    ultimately show ?thesis by blast
     1.5  qed
     1.6  
     1.7 -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")
     1.8 +lemma INum_normNum_iff: "(INum x ::'a::{field, division_by_zero, ring_char_0}) = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
     1.9  proof -
    1.10    have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
    1.11      by (simp del: normNum)