equal
deleted
inserted
replaced
130 blast_tac (HOL_cs addIs |
130 blast_tac (HOL_cs addIs |
131 [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans, |
131 [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans, |
132 rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *}) |
132 rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *}) |
133 apply (erule rtrancl_induct) |
133 apply (erule rtrancl_induct) |
134 apply blast |
134 apply blast |
135 apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans) |
135 apply (blast del: rtrancl_refl intro: rtranclIs) |
136 done |
136 done |
137 |
137 |
138 end |
138 end |