--- a/src/HOL/Isar_Examples/Basic_Logic.thy Fri Feb 21 17:06:48 2014 +0100
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy Fri Feb 21 18:23:11 2014 +0100
@@ -291,7 +291,7 @@
cases actually coincide. Consequently the proof may be rephrased as
follows. *}
-lemma "P \<or> P --> P"
+lemma "P \<or> P \<longrightarrow> P"
proof
assume "P \<or> P"
then show P
@@ -307,7 +307,7 @@
are implicitly performed when concluding the single rule step of the
double-dot proof as follows. *}
-lemma "P \<or> P --> P"
+lemma "P \<or> P \<longrightarrow> P"
proof
assume "P \<or> P"
then show P ..