doc-src/Ref/simplifier-eg.txt
changeset 4396 d103e5e164f8
parent 359 b5a2e9503a7a
equal deleted inserted replaced
4395:a2b726277050 4396:d103e5e164f8
       
     1 
     1 Pretty.setmargin 70;
     2 Pretty.setmargin 70;
       
     3 
       
     4 
       
     5 context Arith.thy;
       
     6 goal Arith.thy "0 + (x + 0) = x + 0 + 0";
       
     7 by (Simp_tac 1);
       
     8 
       
     9 
       
    10 
     2 
    11 
     3 > goal Nat.thy "m+0 = m";
    12 > goal Nat.thy "m+0 = m";
     4 Level 0
    13 Level 0
     5 m + 0 = m
    14 m + 0 = m
     6  1. m + 0 = m
    15  1. m + 0 = m