# HG changeset patch
# User paulson
# Date 882873618 -3600
# Node ID bd05e2a28602a843c7e567da2cdcfbb5eb63a7ef
# Parent  305390f23734394309760017096312946aa662f9
New rules rev_iffD{1,2}

diff -r 305390f23734 -r bd05e2a28602 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Tue Dec 23 11:39:03 1997 +0100
+++ b/src/HOL/HOL.ML	Tue Dec 23 11:40:18 1997 +0100
@@ -64,7 +64,11 @@
  (fn prems =>
         [rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]);
 
-val iffD1 = sym RS iffD2;
+qed_goal "rev_iffD2" HOL.thy "!!P. [| Q; P=Q |] ==> P"
+ (fn _ => [etac iffD2 1, assume_tac 1]);
+
+bind_thm ("iffD1", sym RS iffD2);
+bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2));
 
 qed_goal "iffE" HOL.thy
     "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"