| changeset 59807 | 22bc39064290 |
| parent 58889 | 5b7a9633cfa8 |
| child 60148 | f0fc2378a479 |
--- a/src/HOL/Wellfounded.thy Wed Mar 25 10:41:53 2015 +0100 +++ b/src/HOL/Wellfounded.thy Wed Mar 25 10:44:57 2015 +0100 @@ -232,7 +232,7 @@ prefer 2 apply blast apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE) apply assumption -apply (erule_tac V = "ALL Q. (EX x. x : Q) --> ?P Q" in thin_rl) +apply (erule_tac V = "ALL Q. (EX x. x : Q) --> P Q" for P in thin_rl) --{*essential for speed*} txt{*Blast with new substOccur fails*} apply (fast intro: converse_rtrancl_into_rtrancl)