diff -r fa3c214559b0 -r b1b47d28c295 thys2/UF_Rec.thy
--- a/thys2/UF_Rec.thy	Sat May 25 11:46:25 2013 +0100
+++ b/thys2/UF_Rec.thy	Sat May 25 16:40:48 2013 +0100
@@ -291,9 +291,9 @@
   "Std cf = (left_std (Left cf) \<and> right_std (Right cf))"
 
 text{* 
-  @{text "Nostop m cf k"} means that afer @{text k} steps of 
+  @{text "Stop m cf k"} means that afer @{text k} steps of 
   execution the TM coded by @{text m} and started in configuration
-  @{text cf} is not at a stardard final configuration. *}
+  @{text cf} is in a stardard final configuration. *}
 
 fun Final :: "nat \<Rightarrow> bool"
   where