src/HOL/Isar_Examples/Peirce.thy

   the negated goal may be introduced as additional assumption.  This
   eventually leads to a contradiction.\footnote{The rule involved
   there is negation elimination; it holds in intuitionistic logic as
   well.} *}
 
-theorem "((A --> B) --> A) --> A"
+theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
 proof
-  assume "(A --> B) --> A"
+  assume "(A \<longrightarrow> B) \<longrightarrow> A"
   show A
   proof (rule classical)
-    assume "~ A"
-    have "A --> B"
+    assume "\<not> A"
+    have "A \<longrightarrow> B"
     proof
       assume A
-      with `~ A` show B by contradiction
+      with `\<not> A` show B by contradiction
     qed
-    with `(A --> B) --> A` show A ..
+    with `(A \<longrightarrow> B) \<longrightarrow> A` show A ..
   qed
 qed
 
 text {* In the subsequent version the reasoning is rearranged by means
   of ``weak assumptions'' (as introduced by \isacommand{presume}).

   \isacommand{show} in the context of weak assumptions then the latter
   give rise to new subgoals, which may be established separately.  In
   contrast, strong assumptions (as introduced by \isacommand{assume})
   are solved immediately. *}
 
-theorem "((A --> B) --> A) --> A"
+theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
 proof
-  assume "(A --> B) --> A"
+  assume "(A \<longrightarrow> B) \<longrightarrow> A"
   show A
   proof (rule classical)
-    presume "A --> B"
-    with `(A --> B) --> A` show A ..
+    presume "A \<longrightarrow> B"
+    with `(A \<longrightarrow> B) \<longrightarrow> A` show A ..
   next
-    assume "~ A"
-    show "A --> B"
+    assume "\<not> A"
+    show "A \<longrightarrow> B"
     proof
       assume A
-      with `~ A` show B by contradiction
+      with `\<not> A` show B by contradiction
     qed
   qed
 qed
 
 text {* Note that the goals stemming from weak assumptions may be even