# HG changeset patch
# User nipkow
# Date 1492677952 -7200
# Node ID d10f0bbc7ea152fb2fa1ab4fb06404080dbc7d16
# Parent  587433a18053c486a855c97f9cc0772bb273efdf
typo

diff -r 587433a18053 -r d10f0bbc7ea1 src/Doc/Prog_Prove/Bool_nat_list.thy
--- 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
 %