typo

--- a/src/Doc/Prog_Prove/Bool_nat_list.thy	Wed Apr 19 16:26:09 2017 +0200
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy	Thu Apr 20 10:45:52 2017 +0200
@@ -416,7 +416,7 @@
 @{prop"tl(x#xs) = xs"}
 \end{isabelle}
 Note that since HOL is a logic of total functions, @{term"hd []"} is defined,
-but we do now know what the result is. That is, @{term"hd []"} is not undefined
+but we do not know what the result is. That is, @{term"hd []"} is not undefined
 but underdefined.
 \fi
 %