equal
deleted
inserted
replaced
230 apply blast |
230 apply blast |
231 apply (case_tac "y:Q") |
231 apply (case_tac "y:Q") |
232 prefer 2 apply blast |
232 prefer 2 apply blast |
233 apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE) |
233 apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE) |
234 apply assumption |
234 apply assumption |
235 apply (erule_tac V = "ALL Q. (EX x. x : Q) --> ?P Q" in thin_rl) |
235 apply (erule_tac V = "ALL Q. (EX x. x : Q) --> P Q" for P in thin_rl) |
236 --{*essential for speed*} |
236 --{*essential for speed*} |
237 txt{*Blast with new substOccur fails*} |
237 txt{*Blast with new substOccur fails*} |
238 apply (fast intro: converse_rtrancl_into_rtrancl) |
238 apply (fast intro: converse_rtrancl_into_rtrancl) |
239 done |
239 done |
240 |
240 |