1.1 --- a/doc-src/Ref/simplifier-eg.txt	Tue May 03 18:36:18 1994 +0200
     1.2 +++ b/doc-src/Ref/simplifier-eg.txt	Tue May 03 18:38:28 1994 +0200
     1.3 @@ -1,3 +1,5 @@
     1.4 +Pretty.setmargin 70;
     1.5 +
     1.6  > goal Nat.thy "m+0 = m";
     1.7  Level 0
     1.8  m + 0 = m
     1.9 @@ -71,3 +73,39 @@
    1.10  Level 3
    1.11  f(i + j) = i + f(j)
    1.12  No subgoals!
    1.13 +
    1.14 +
    1.15 +
    1.16 +> goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)";
    1.17 +Level 0
    1.18 +Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
    1.19 + 1. Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
    1.20 +
    1.21 +> by (simp_tac natsum_ss 1);
    1.22 +Level 1
    1.23 +Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
    1.24 + 1. n + (n + (sum(%i. i, n) + sum(%i. i, n))) = n + n * n
    1.25 +
    1.26 +> by (nat_ind_tac "n" 1);
    1.27 +Level 2
    1.28 +Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
    1.29 + 1. 0 + (0 + (sum(%i. i, 0) + sum(%i. i, 0))) = 0 + 0 * 0
    1.30 + 2. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) =
    1.31 +          n1 + n1 * n1 ==>
    1.32 +          Suc(n1) +
    1.33 +          (Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) =
    1.34 +          Suc(n1) + Suc(n1) * Suc(n1)
    1.35 +
    1.36 +> by (simp_tac natsum_ss 1);
    1.37 +Level 3
    1.38 +Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
    1.39 + 1. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) =
    1.40 +          n1 + n1 * n1 ==>
    1.41 +          Suc(n1) +
    1.42 +          (Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) =
    1.43 +          Suc(n1) + Suc(n1) * Suc(n1)
    1.44 +
    1.45 +> by (asm_simp_tac natsum_ss 1);
    1.46 +Level 4
    1.47 +Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
    1.48 +No subgoals!