author | haftmann |
Tue, 07 Feb 2017 22:15:04 +0100 | |
changeset 64996 | b316cd527a11 |
parent 64995 | a7af4045f873 |
child 64997 | 067a6cca39f0 |
src/HOL/Int.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Int.thy Tue Feb 07 22:15:03 2017 +0100 +++ b/src/HOL/Int.thy Tue Feb 07 22:15:04 2017 +0100 @@ -1721,7 +1721,7 @@ text \<open>Implementations.\<close> -lemma one_int_code [code, code_unfold]: "1 = Pos Num.One" +lemma one_int_code [code]: "1 = Pos Num.One" by simp lemma plus_int_code [code]: