added lemma;

--- a/src/HOL/ex/Higher_Order_Logic.thy	Thu Dec 20 21:14:59 2001 +0100
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Thu Dec 20 21:15:37 2001 +0100
@@ -308,4 +308,15 @@
   qed
 qed
 
+lemma (in classical) "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"  (* FIXME *)
+proof -
+  assume r: "\<not> A \<Longrightarrow> A"
+  show A
+  proof (rule classical_cases)
+    assume A thus A .
+  next
+    assume "\<not> A" thus A by (rule r)
+  qed
+qed
+
 end