src/HOL/Isar_Examples/Basic_Logic.thy

 
   \medskip In our example the situation is even simpler, since the two
   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
   proof
     assume P

 text {* Again, the rather vacuous body of the proof may be collapsed.
   Thus the case analysis degenerates into two assumption steps, which
   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 ..
 qed