tuned;

--- a/doc-src/Ref/simplifier-eg.txt	Fri Dec 12 17:11:05 1997 +0100
+++ b/doc-src/Ref/simplifier-eg.txt	Fri Dec 12 17:11:26 1997 +0100
@@ -1,5 +1,14 @@
+
 Pretty.setmargin 70;
 
+
+context Arith.thy;
+goal Arith.thy "0 + (x + 0) = x + 0 + 0";
+by (Simp_tac 1);
+
+
+
+
 > goal Nat.thy "m+0 = m";
 Level 0
 m + 0 = m