changeset 6046 | 2c8a8be36c94 |
parent 5529 | 4a54acae6a15 |
child 6070 | 032babd0120b |
--- a/src/ZF/ex/Limit.ML Mon Dec 28 16:53:24 1998 +0100 +++ b/src/ZF/ex/Limit.ML Mon Dec 28 16:54:01 1998 +0100 @@ -312,8 +312,7 @@ val Yub = rewrite_rule[islub_def]Ylub RS conjunct1; val Xub_y = Yub RS (dom RS dominate_isub); val lem = Xub_y RS (rewrite_rule[islub_def]Xlub RS conjunct2 RS spec RS mp); -val thm = Y RS (X RS (cpo RS lem)); -by (rtac thm 1); +by (rtac (Y RS (X RS (cpo RS lem))) 1); qed "dominate_islub"; val prems = Goalw [subchain_def] (* subchainE *)