diff -r 846c72206207 -r b3eb789616c3 src/HOL/Isar_Examples/Basic_Logic.thy
--- a/src/HOL/Isar_Examples/Basic_Logic.thy	Mon Nov 02 13:58:19 2015 +0100
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy	Mon Nov 02 14:09:14 2015 +0100
@@ -253,9 +253,7 @@
 proof
   assume "P \<or> P"
   then show P
-  proof                    -- \<open>
-    rule \<open>disjE\<close>: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
-\<close>
+  proof                    -- \<open>rule \<open>disjE\<close>: \smash{$\infer{\<open>C\<close>}{\<open>A \<or> B\<close> & \infer*{\<open>C\<close>}{[\<open>A\<close>]} & \infer*{\<open>C\<close>}{[\<open>B\<close>]}}$}\<close>
     assume P show P by fact
   next
     assume P show P by fact
@@ -324,8 +322,7 @@
 proof
   assume "\<exists>x. P (f x)"
   then show "\<exists>y. P y"
-  proof (rule exE)             --
-    \<open>rule \<open>exE\<close>: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}\<close>
+  proof (rule exE)             -- \<open>rule \<open>exE\<close>: \smash{$\infer{\<open>B\<close>}{\<open>\<exists>x. A(x)\<close> & \infer*{\<open>B\<close>}{[\<open>A(x)\<close>]_x}}$}\<close>
     fix a
     assume "P (f a)" (is "P ?witness")
     then show ?thesis by (rule exI [of P ?witness])