--- a/src/HOL/Isar_Examples/Structured_Statements.thy Mon Jun 22 19:22:48 2015 +0200
+++ b/src/HOL/Isar_Examples/Structured_Statements.thy Mon Jun 22 20:36:33 2015 +0200
@@ -130,4 +130,33 @@
qed
end
-end
\ No newline at end of file
+
+subsection \<open>Suffices-to-show\<close>
+
+notepad
+begin
+ fix A B C
+ assume r: "A \<Longrightarrow> B \<Longrightarrow> C"
+
+ have C
+ proof -
+ show ?thesis when A (is ?A) and B (is ?B)
+ using that by (rule r)
+ show ?A sorry
+ show ?B sorry
+ qed
+next
+ fix a :: 'a
+ fix A :: "'a \<Rightarrow> bool"
+ fix C
+
+ have C
+ proof -
+ show ?thesis when "A x" (is ?A) for x :: 'a -- \<open>abstract @{term x}\<close>
+ using that sorry
+ show "?A a" -- \<open>concrete @{term a}\<close>
+ sorry
+ qed
+end
+
+end