src/FOL/FOL.thy

--- a/src/FOL/FOL.thy	Wed Mar 26 22:39:58 2008 +0100
+++ b/src/FOL/FOL.thy	Wed Mar 26 22:40:01 2008 +0100
@@ -163,6 +163,12 @@
   qed
 qed
 
+lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
+  by (rule classical) iprover
+
+lemma swap: "~ P ==> (~ R ==> P) ==> R"
+  by (rule classical) iprover
+
 use "cladata.ML"
 setup Cla.setup
 setup cla_setup