dropped superfluous preprocessing rule
authorhaftmann
Tue Feb 07 22:15:04 2017 +0100 (2017-02-07)
changeset 64996b316cd527a11
parent 64995 a7af4045f873
child 64997 067a6cca39f0
dropped superfluous preprocessing rule
src/HOL/Int.thy
     1.1 --- a/src/HOL/Int.thy	Tue Feb 07 22:15:03 2017 +0100
     1.2 +++ b/src/HOL/Int.thy	Tue Feb 07 22:15:04 2017 +0100
     1.3 @@ -1721,7 +1721,7 @@
     1.4  
     1.5  text \<open>Implementations.\<close>
     1.6  
     1.7 -lemma one_int_code [code, code_unfold]: "1 = Pos Num.One"
     1.8 +lemma one_int_code [code]: "1 = Pos Num.One"
     1.9    by simp
    1.10  
    1.11  lemma plus_int_code [code]: