doc-src/TutorialI/Advanced/WFrec.thy

--- a/doc-src/TutorialI/Advanced/WFrec.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -90,19 +90,10 @@
 
 \noindent
 The inclusion remains to be proved. After unfolding some definitions, 
-we are left with simple arithmetic:
+we are left with simple arithmetic that is dispatched automatically.
 *}
 
-apply (clarify, simp add: measure_def inv_image_def)
-
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-
-\noindent
-And that is dispatched automatically:
-*}
-
-by arith
+by (clarify, simp add: measure_def inv_image_def)
 
 text{*\noindent