# HG changeset patch
# User paulson
# Date 882785807 -3600
# Node ID fefe21f761d79d1792016787da81ba79e9981421
# Parent  a98605717d837f53b319b282e96b86ed60dec4ba
New rules rev_iffD{1,2}

diff -r a98605717d83 -r fefe21f761d7 src/FOL/IFOL.ML
--- a/src/FOL/IFOL.ML	Fri Dec 19 19:59:50 1997 +0100
+++ b/src/FOL/IFOL.ML	Mon Dec 22 11:16:47 1997 +0100
@@ -103,6 +103,12 @@
 qed_goalw "iffD2" IFOL.thy [iff_def] "[| P <-> Q;  Q |] ==> P"
  (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);
 
+qed_goal "rev_iffD1" IFOL.thy "!!P. [| P; P <-> Q |] ==> Q"
+ (fn _ => [etac iffD1 1, assume_tac 1]);
+
+qed_goal "rev_iffD2" IFOL.thy "!!P. [| Q; P <-> Q |] ==> P"
+ (fn _ => [etac iffD2 1, assume_tac 1]);
+
 qed_goal "iff_refl" IFOL.thy "P <-> P"
  (fn _ => [ (REPEAT (ares_tac [iffI] 1)) ]);