src/HOL/HOL.ML
changeset 4467 bd05e2a28602
parent 4302 2c99775d953f
child 4527 4878fb3d0ac5
     1.1 --- a/src/HOL/HOL.ML	Tue Dec 23 11:39:03 1997 +0100
     1.2 +++ b/src/HOL/HOL.ML	Tue Dec 23 11:40:18 1997 +0100
     1.3 @@ -64,7 +64,11 @@
     1.4   (fn prems =>
     1.5          [rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]);
     1.6  
     1.7 -val iffD1 = sym RS iffD2;
     1.8 +qed_goal "rev_iffD2" HOL.thy "!!P. [| Q; P=Q |] ==> P"
     1.9 + (fn _ => [etac iffD2 1, assume_tac 1]);
    1.10 +
    1.11 +bind_thm ("iffD1", sym RS iffD2);
    1.12 +bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2));
    1.13  
    1.14  qed_goal "iffE" HOL.thy
    1.15      "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"