--- a/doc-src/TutorialI/Trie/Trie.thy Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Trie/Trie.thy Thu Jan 25 15:31:31 2001 +0100
@@ -132,7 +132,7 @@
proof states are invisible, and we rely on the (possibly brittle) magic of
@{text auto} (@{text simp_all} will not do --- try it) to split the subgoals
of the induction up in such a way that case distinction on @{term bs} makes
-sense and solves the proof. Part~\ref{Isar} shows you how to write readable
+sense and solves the proof. Chapter~\ref{ch:Isar} shows you how to write readable
and stable proofs.
*};