diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Trie/document/Trie.tex --- a/doc-src/TutorialI/Trie/document/Trie.tex Thu Jan 25 11:59:52 2001 +0100 +++ b/doc-src/TutorialI/Trie/document/Trie.tex Thu Jan 25 15:31:31 2001 +0100 @@ -122,7 +122,7 @@ proof states are invisible, and we rely on the (possibly brittle) magic of \isa{auto} (\isa{simp{\isacharunderscore}all} will not do --- try it) to split the subgoals of the induction up in such a way that case distinction on \isa{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.% \end{isamarkuptext}% \end{isabellebody}%