| changeset 4467 | bd05e2a28602 |
| parent 4302 | 2c99775d953f |
| child 4527 | 4878fb3d0ac5 |
--- 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"