doc-src/TutorialI/Overview/Isar0.thy

--- a/doc-src/TutorialI/Overview/Isar0.thy	Mon Jul 01 12:50:35 2002 +0200
+++ b/doc-src/TutorialI/Overview/Isar0.thy	Mon Jul 01 15:33:03 2002 +0200
@@ -305,4 +305,22 @@
 theorem "EX S. S ~: range (f :: 'a => 'a set)"
   by best
 
+(* Finally, whole scripts may appear in the leaves of the proof tree,
+although this is best avoided. Here is a contrived example. *)
+
+lemma "A \<longrightarrow> (A \<longrightarrow>B) \<longrightarrow> B"
+proof
+  assume A: A
+  show "(A \<longrightarrow>B) \<longrightarrow> B"
+    apply(rule impI)
+    apply(erule impE)
+    apply(rule A)
+    apply assumption
+    done
+qed
+
+
+(* You may need to resort to this technique if an automatic step fails to
+prove the desired proposition. *)
+
 end