author | oheimb |
Tue, 24 Mar 1998 15:49:32 +0100 | |
changeset 4751 | 6fbd9838ccae |
parent 4750 | f83cd6a06676 |
child 4752 | 1c334bd00038 |
src/HOL/WF_Rel.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/WF_Rel.ML Tue Mar 24 15:46:34 1998 +0100 +++ b/src/HOL/WF_Rel.ML Tue Mar 24 15:49:32 1998 +0100 @@ -118,7 +118,7 @@ qed_spec_mp "finite_acyclic_wf"; qed_goal "finite_acyclic_wf_converse" thy - "ÄX. Ëfinite r; acyclic rÌ êë wf (r^-1)" (K [ + "!!X. [|finite r; acyclic r|] ==> wf (r^-1)" (K [ etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1, etac (acyclic_converse RS iffD2) 1]);