# HG changeset patch
# User wenzelm
# Date 1455464400 -3600
# Node ID ec0fbd1a852bd987eced9dcf4adc660200833ab6
# Parent  aaeee16a56f5edbdd034a2fcc58e48ed326d6d2a
more explicit dummy proofs;

diff -r aaeee16a56f5 -r ec0fbd1a852b src/HOL/Isar_Examples/Structured_Statements.thy
--- a/src/HOL/Isar_Examples/Structured_Statements.thy	Sun Feb 14 16:39:43 2016 +0100
+++ b/src/HOL/Isar_Examples/Structured_Statements.thy	Sun Feb 14 16:40:00 2016 +0100
@@ -17,17 +17,17 @@
 
   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
 
@@ -40,8 +40,8 @@
 
   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
@@ -86,16 +86,16 @@
   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"
@@ -107,10 +107,10 @@
   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
 
@@ -124,9 +124,9 @@
 
   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
 
@@ -142,8 +142,8 @@
   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
@@ -153,9 +153,9 @@
   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
 
diff -r aaeee16a56f5 -r ec0fbd1a852b src/HOL/Isar_Examples/document/root.tex
--- a/src/HOL/Isar_Examples/document/root.tex	Sun Feb 14 16:39:43 2016 +0100
+++ b/src/HOL/Isar_Examples/document/root.tex	Sun Feb 14 16:40:00 2016 +0100
@@ -5,10 +5,6 @@
 \isabellestyle{it}
 \usepackage{pdfsetup}\urlstyle{rm}
 
-\renewcommand{\isacommand}[1]
-{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
-  {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
-
 \newcommand{\DUMMYPROOF}{{\langle\mathit{proof}\rangle}}
 \newcommand{\dummyproof}{$\DUMMYPROOF$}