--- 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