doc-src/TutorialI/Types/Numbers.thy

--- a/doc-src/TutorialI/Types/Numbers.thy	Wed Aug 08 14:33:10 2001 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy	Wed Aug 08 14:50:28 2001 +0200
@@ -83,8 +83,10 @@
 *}
 
 
-lemma "(n-1)*(n+1) = n*n - 1"
-apply (simp split: nat_diff_split)
+lemma "(n-#2)*(n+#2) = n*n - (#4::nat)"
+apply (clarsimp split: nat_diff_split)
+ --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (subgoal_tac "n=0 | n=1", force, arith)
 done
 
 text{*