equal
deleted
inserted
replaced
64 Goalw [le_dual_def] "x [= (x::'a::quasi_order dual)"; |
64 Goalw [le_dual_def] "x [= (x::'a::quasi_order dual)"; |
65 by (rtac le_refl 1); |
65 by (rtac le_refl 1); |
66 qed "le_dual_refl"; |
66 qed "le_dual_refl"; |
67 |
67 |
68 Goalw [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)"; |
68 Goalw [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)"; |
69 by (stac conj_commut 1); |
69 br impI 1; |
70 by (rtac le_trans 1); |
70 br (le_trans RS mp) 1; |
|
71 by (Blast_tac 1); |
71 qed "le_dual_trans"; |
72 qed "le_dual_trans"; |
72 |
73 |
73 Goalw [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)"; |
74 Goalw [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)"; |
74 by Safe_tac; |
75 by Safe_tac; |
75 by (rtac (Rep_dual_inverse RS subst) 1); |
76 by (rtac (Rep_dual_inverse RS subst) 1); |