Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
blast_tac -> blast in comment (fix latex error)
authorkleing
Tue, 30 Nov 2004 06:50:03 +0100
changeset 15343 444bb25d3da0
parent 15342 13bd3d12ec2f
child 15344 d371b50fcf82
blast_tac -> blast in comment (fix latex error)
src/HOL/Wellfounded_Recursion.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle