# HG changeset patch
# User wenzelm
# Date 1008879337 -3600
# Node ID 6226b35c04ca08a5843d57a2ac68c4388a7a8d65
# Parent  f8ad8cfb83092dd4603bc790b76419ca49d144cc
added lemma;

diff -r f8ad8cfb8309 -r 6226b35c04ca src/HOL/ex/Higher_Order_Logic.thy
--- 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