changeset 15343 | 444bb25d3da0 |
parent 15341 | 254f6f00b60e |
child 15950 | 5c067c956a20 |
--- a/src/HOL/Wellfounded_Recursion.thy Mon Nov 29 18:49:35 2004 +0100 +++ b/src/HOL/Wellfounded_Recursion.thy Tue Nov 30 06:50:03 2004 +0100 @@ -131,7 +131,7 @@ apply assumption apply (erule_tac V = "ALL Q. (EX x. x : Q) --> ?P Q" in thin_rl) --{*essential for speed*} -txt{*Blast_tac with new substOccur fails*} +txt{*Blast with new substOccur fails*} apply (fast intro: converse_rtrancl_into_rtrancl) done