src/HOL/Isar_examples/Peirce.thy

  is negation elimination; it holds in intuitionistic logic as well.}
 *}
 
 theorem "((A --> B) --> A) --> A"
 proof
-  assume aba: "(A --> B) --> A"
+  assume "(A --> B) --> A"
   show A
   proof (rule classical)
     assume "~ A"
     have "A --> B"
     proof
       assume A
-      thus B by contradiction
+      with `~ A` show B by contradiction
     qed
-    with aba show A ..
+    with `(A --> B) --> A` show A ..
   qed
 qed
 
 text {*
  In the subsequent version the reasoning is rearranged by means of

  are solved immediately.
 *}
 
 theorem "((A --> B) --> A) --> A"
 proof
-  assume aba: "(A --> B) --> A"
+  assume "(A --> B) --> A"
   show A
   proof (rule classical)
     presume "A --> B"
-    with aba show A ..
+    with `(A --> B) --> A` show A ..
   next
     assume "~ A"
     show "A --> B"
     proof
       assume A
-      thus B by contradiction
+      with `~ A` show B by contradiction
     qed
   qed
 qed
 
 text {*