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