iff del: less_Suc0 -- luckily this does NOT affect the printed text;

--- a/doc-src/TutorialI/Types/Numbers.thy	Wed Jan 23 17:13:54 2002 +0100
+++ b/doc-src/TutorialI/Types/Numbers.thy	Thu Jan 24 16:37:43 2002 +0100
@@ -84,7 +84,7 @@
 
 
 lemma "(n - 1) * (n + 1) = n * n - (1::nat)"
-apply (clarsimp split: nat_diff_split)
+apply (clarsimp split: nat_diff_split iff del: less_Suc0)
  --{* @{subgoals[display,indent=0,margin=65]} *}
 apply (subgoal_tac "n=0", force, arith)
 done