src/HOL/Int.thy
changeset 48044 fea6f3060b65
parent 47255 30a1692557b0
child 48045 fbf77fdf9ae4
equal deleted inserted replaced
48043:3ff2c76c9f64 48044:fea6f3060b65
   868 by arith
   868 by arith
   869 
   869 
   870 
   870 
   871 subsection{*The functions @{term nat} and @{term int}*}
   871 subsection{*The functions @{term nat} and @{term int}*}
   872 
   872 
   873 text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
   873 text{*Simplify the term @{term "w + - z"}*}
   874   @{term "w + - z"}*}
       
   875 declare Zero_int_def [symmetric, simp]
       
   876 declare One_int_def [symmetric, simp]
       
   877 
       
   878 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
   874 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
   879 
   875 
   880 lemma nat_0 [simp]: "nat 0 = 0"
   876 lemma nat_0 [simp]: "nat 0 = 0"
   881 by (simp add: nat_eq_iff)
   877 by (simp add: nat_eq_iff)
   882 
   878