src/HOL/Isar_Examples/Structured_Statements.thy

   fix A B :: bool
   fix P :: "'a \<Rightarrow> bool"
 
   have "A \<longrightarrow> B"
   proof
-    show B if A using that sorry
+    show B if A using that \<proof>
   qed
 
   have "\<not> A"
   proof
-    show False if A using that sorry
+    show False if A using that \<proof>
   qed
 
   have "\<forall>x. P x"
   proof
-    show "P x" for x sorry
+    show "P x" for x \<proof>
   qed
 end
 
 
 subsection \<open>If-and-only-if\<close>

 begin
   fix A B :: bool
 
   have "A \<longleftrightarrow> B"
   proof
-    show B if A sorry
-    show A if B sorry
+    show B if A \<proof>
+    show A if B \<proof>
   qed
 next
   fix A B :: bool
 
   have iff_comm: "(A \<and> B) \<longleftrightarrow> (B \<and> A)"

   consider (a) A | (b) B | (c) C | (d) D
     using * by blast
   then have something
   proof cases
     case a  thm \<open>A\<close>
-    then show ?thesis sorry
+    then show ?thesis \<proof>
   next
     case b  thm \<open>B\<close>
-    then show ?thesis sorry
+    then show ?thesis \<proof>
   next
     case c  thm \<open>C\<close>
-    then show ?thesis sorry
+    then show ?thesis \<proof>
   next
     case d  thm \<open>D\<close>
-    then show ?thesis sorry
+    then show ?thesis \<proof>
   qed
 next
   fix A :: "'a \<Rightarrow> bool"
   fix B :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
   assume *: "(\<exists>x. A x) \<or> (\<exists>y z. B y z)"

   consider (a) x where "A x" | (b) y z where "B y z"
     using * by blast
   then have something
   proof cases
     case a  thm \<open>A x\<close>
-    then show ?thesis sorry
+    then show ?thesis \<proof>
   next
     case b  thm \<open>B y z\<close>
-    then show ?thesis sorry
+    then show ?thesis \<proof>
   qed
 end
 
 
 subsection \<open>Induction\<close>

   fix P :: "nat \<Rightarrow> bool"
   fix n :: nat
 
   have "P n"
   proof (induct n)
-    show "P 0" sorry
+    show "P 0" \<proof>
     show "P (Suc n)" if "P n" for n  thm \<open>P n\<close>
-      using that sorry
+      using that \<proof>
   qed
 end
 
 
 subsection \<open>Suffices-to-show\<close>

 
   have C
   proof -
     show ?thesis when A (is ?A) and B (is ?B)
       using that by (rule r)
-    show ?A sorry
-    show ?B sorry
+    show ?A \<proof>
+    show ?B \<proof>
   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  \<comment> \<open>abstract @{term x}\<close>
-      using that sorry
+      using that \<proof>
     show "?A a"  \<comment> \<open>concrete @{term a}\<close>
-      sorry
+      \<proof>
   qed
 end
 
 end