equal
deleted
inserted
replaced
538 by (rtac (thm "f_cl" RS CLF_dual) 1); |
538 by (rtac (thm "f_cl" RS CLF_dual) 1); |
539 by (afs [dualr_iff] 1); |
539 by (afs [dualr_iff] 1); |
540 qed "T_thm_1_glb"; |
540 qed "T_thm_1_glb"; |
541 |
541 |
542 (* interval *) |
542 (* interval *) |
543 Goal "refl A r ==> r <= A Times A"; |
543 Goal "refl A r ==> r <= A <*> A"; |
544 by (afs [refl_def] 1); |
544 by (afs [refl_def] 1); |
545 qed "reflE1"; |
545 qed "reflE1"; |
546 |
546 |
547 Goal "(x, y): r ==> x: A"; |
547 Goal "(x, y): r ==> x: A"; |
548 by (rtac SigmaD1 1); |
548 by (rtac SigmaD1 1); |