# HG changeset patch
# User kleing
# Date 1101793803 -3600
# Node ID 444bb25d3da0f22a4581e4f614475602b83ced24
# Parent  13bd3d12ec2fdda0636343dcb068fedf7977e6e7
blast_tac -> blast in comment (fix latex error)

diff -r 13bd3d12ec2f -r 444bb25d3da0 src/HOL/Wellfounded_Recursion.thy
--- 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