# HG changeset patch
# User nipkow
# Date 907259365 -7200
# Node ID 6b8dee1a6ebb8263d1cadfa24761be844e794f36
# Parent  a12b25c53df11fac59c7b6369fdac655566bb808
a few new lemmas.

diff -r a12b25c53df1 -r 6b8dee1a6ebb src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Thu Oct 01 18:28:47 1998 +0200
+++ b/src/HOL/Arith.ML	Thu Oct 01 18:29:25 1998 +0200
@@ -93,11 +93,27 @@
 (** Reasoning about m+0=0, etc. **)
 
 Goal "(m+n = 0) = (m=0 & n=0)";
-by (induct_tac "m" 1);
-by (ALLGOALS Asm_simp_tac);
+by (exhaust_tac "m" 1);
+by (Auto_tac);
 qed "add_is_0";
 AddIffs [add_is_0];
 
+Goal "(0 = m+n) = (m=0 & n=0)";
+by (exhaust_tac "m" 1);
+by (Auto_tac);
+qed "zero_is_add";
+AddIffs [zero_is_add];
+
+Goal "(m+n=1) = (m=1 & n=0 | m=0 & n=1)";
+by(exhaust_tac "m" 1);
+by(Auto_tac);
+qed "add_is_1";
+
+Goal "(1=m+n) = (m=1 & n=0 | m=0 & n=1)";
+by(exhaust_tac "m" 1);
+by(Auto_tac);
+qed "one_is_add";
+
 Goal "(0<m+n) = (0<m | 0<n)";
 by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
 qed "add_gr_0";