# HG changeset patch
# User wenzelm
# Date 881943086 -3600
# Node ID d103e5e164f82e4d68411cfc538b431ac178769d
# Parent  a2b7262770508c213a1083ffe198aa08cb2e2f73
tuned;

diff -r a2b726277050 -r d103e5e164f8 doc-src/Ref/simplifier-eg.txt
--- 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