doc-src/TutorialI/Trie/document/Trie.tex
changeset 10971 6852682eaf16
parent 10795 9e888d60d3e5
child 10978 5eebea8f359f
     1.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -120,7 +120,7 @@
     1.4  This proof may look surprisingly straightforward. However, note that this
     1.5  comes at a cost: the proof script is unreadable because the intermediate
     1.6  proof states are invisible, and we rely on the (possibly brittle) magic of
     1.7 -\isa{auto} (\isa{simp{\isacharunderscore}all} will not do---try it) to split the subgoals
     1.8 +\isa{auto} (\isa{simp{\isacharunderscore}all} will not do --- try it) to split the subgoals
     1.9  of the induction up in such a way that case distinction on \isa{bs} makes
    1.10  sense and solves the proof. Part~\ref{Isar} shows you how to write readable
    1.11  and stable proofs.%