# HG changeset patch
# User paulson
# Date 956066071 -7200
# Node ID e583d8987abb91123481d7f13288b2c03657a5cb
# Parent  f9733879ff25928923591bc514099d0468ad840f
tidied

diff -r f9733879ff25 -r e583d8987abb src/HOL/Algebra/abstract/NatSum.ML
--- a/src/HOL/Algebra/abstract/NatSum.ML	Tue Apr 18 15:53:50 2000 +0200
+++ b/src/HOL/Algebra/abstract/NatSum.ML	Tue Apr 18 15:54:31 2000 +0200
@@ -87,10 +87,8 @@
 
 section "Results for the Construction of Polynomials";
 
-goal Main.thy (* could go to Arith *)
-  "!!j::nat. [| m <= j; Suc j <= n |] ==> (n - m) - Suc (j - m) = n - Suc j";
-by (asm_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1);
-by (asm_simp_tac (simpset() addsimps [diff_right_cancel, less_imp_le]) 1);
+Goal "[| m <= j; Suc j <= n |] ==> (n - m) - Suc (j - m) = n - Suc j";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split']) 1);
 qed "Suc_diff_lemma";
 
 Goal
@@ -105,8 +103,11 @@
 by (etac impE 1);
 by (rtac Suc_leD 1);
 by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps a_ac@[Suc_diff_le, l_distr, r_distr, m_assoc, SUM_add]) 1);
-by (asm_simp_tac (simpset() addsimps a_ac@[Suc_diff_lemma, SUM_ldistr, m_assoc]) 1);
+by (asm_simp_tac
+    (simpset() addsimps a_ac@
+                        [Suc_diff_le, l_distr, r_distr, m_assoc, SUM_add]) 1);
+by (asm_simp_tac
+    (simpset() addsimps a_ac@ [Suc_diff_lemma, SUM_ldistr, m_assoc]) 1);
 qed "poly_assoc_lemma1";
 
 Goal