# HG changeset patch
# User wenzelm
# Date 1082142036 -7200
# Node ID 099575a938e52ce001cec521addc2949e28d4ede
# Parent  0be6c11e71287f8629ce87832c2dd85bf5822cf9
tuned document;

diff -r 0be6c11e7128 -r 099575a938e5 src/HOL/NatArith.thy
--- a/src/HOL/NatArith.thy	Fri Apr 16 21:00:07 2004 +0200
+++ b/src/HOL/NatArith.thy	Fri Apr 16 21:00:36 2004 +0200
@@ -33,12 +33,12 @@
 *}
 (* Careful: arith_tac produces counter examples!
 fun add_arith cs = cs addafter ("arith_tac", arith_tac);
-TODO: use arith_tac for force_tac in Provers/clasip.ML *)
+TODO: use arith_tac for force_tac in Provers/clasimp.ML *)
 
 lemmas [arith_split] = nat_diff_split split_min split_max
 
 
-subsubsection {* Generic summation indexed over natural numbers *}
+subsection {* Generic summation indexed over natural numbers *}
 
 consts
   Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"