equal
deleted
inserted
replaced
136 by (blast_tac (claset() addSIs [rtrancl_subset] |
136 by (blast_tac (claset() addSIs [rtrancl_subset] |
137 addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1); |
137 addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1); |
138 qed "rtrancl_Un_rtrancl"; |
138 qed "rtrancl_Un_rtrancl"; |
139 |
139 |
140 Goal "(R^=)^* = R^*"; |
140 Goal "(R^=)^* = R^*"; |
141 by (blast_tac (claset() addSIs [rtrancl_subset] |
141 by (blast_tac (claset() addSIs [rtrancl_subset] addIs [r_into_rtrancl]) 1); |
142 addIs [rtrancl_refl, r_into_rtrancl]) 1); |
|
143 qed "rtrancl_reflcl"; |
142 qed "rtrancl_reflcl"; |
144 Addsimps [rtrancl_reflcl]; |
143 Addsimps [rtrancl_reflcl]; |
145 |
144 |
146 Goal "(x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1"; |
145 Goal "(x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1"; |
147 by (rtac converseI 1); |
146 by (rtac converseI 1); |