author | huffman |
Wed, 30 May 2012 14:55:44 +0200 | |
changeset 48044 | fea6f3060b65 |
parent 48043 | 3ff2c76c9f64 |
child 48045 | fbf77fdf9ae4 |
src/HOL/Int.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Int.thy Wed May 30 23:10:42 2012 +0200 +++ b/src/HOL/Int.thy Wed May 30 14:55:44 2012 +0200 @@ -870,11 +870,7 @@ subsection{*The functions @{term nat} and @{term int}*} -text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and - @{term "w + - z"}*} -declare Zero_int_def [symmetric, simp] -declare One_int_def [symmetric, simp] - +text{*Simplify the term @{term "w + - z"}*} lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp] lemma nat_0 [simp]: "nat 0 = 0"