New rules rev_iffD{1,2}
authorpaulson
Tue Dec 23 11:40:18 1997 +0100 (1997-12-23)
changeset 4467bd05e2a28602
parent 4466 305390f23734
child 4468 d17524e0beb0
New rules rev_iffD{1,2}
src/HOL/HOL.ML
     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"