doc-src/TutorialI/Trie/Trie.thy
changeset 10978 5eebea8f359f
parent 10971 6852682eaf16
child 11294 16481a4cc9f3
     1.1 --- a/doc-src/TutorialI/Trie/Trie.thy	Thu Jan 25 11:59:52 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Trie/Trie.thy	Thu Jan 25 15:31:31 2001 +0100
     1.3 @@ -132,7 +132,7 @@
     1.4  proof states are invisible, and we rely on the (possibly brittle) magic of
     1.5  @{text auto} (@{text simp_all} will not do --- try it) to split the subgoals
     1.6  of the induction up in such a way that case distinction on @{term bs} makes
     1.7 -sense and solves the proof. Part~\ref{Isar} shows you how to write readable
     1.8 +sense and solves the proof. Chapter~\ref{ch:Isar} shows you how to write readable
     1.9  and stable proofs.
    1.10  *};
    1.11