author | paulson |
Tue, 23 Dec 1997 11:40:18 +0100 | |
changeset 4467 | bd05e2a28602 |
parent 4466 | 305390f23734 |
child 4468 | d17524e0beb0 |
src/HOL/HOL.ML | file | annotate | diff | comparison | revisions |
--- 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"