1.1 --- a/src/HOL/ex/Higher_Order_Logic.thy	Thu Dec 20 21:14:59 2001 +0100
     1.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy	Thu Dec 20 21:15:37 2001 +0100
     1.3 @@ -308,4 +308,15 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma (in classical) "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"  (* FIXME *)
     1.8 +proof -
     1.9 +  assume r: "\<not> A \<Longrightarrow> A"
    1.10 +  show A
    1.11 +  proof (rule classical_cases)
    1.12 +    assume A thus A .
    1.13 +  next
    1.14 +    assume "\<not> A" thus A by (rule r)
    1.15 +  qed
    1.16 +qed
    1.17 +
    1.18  end