src/HOL/Int.thy
changeset 64996 b316cd527a11
parent 64849 766db3539859
child 66035 de6cd60b1226
     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]: