1.1 --- a/doc-src/TutorialI/Trie/Trie.thy Wed Jan 24 11:59:15 2001 +0100
1.2 +++ b/doc-src/TutorialI/Trie/Trie.thy Wed Jan 24 12:29:10 2001 +0100
1.3 @@ -130,7 +130,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 -@{text auto} (@{text simp_all} will not do---try it) to split the subgoals
1.8 +@{text auto} (@{text simp_all} will not do --- try it) to split the subgoals
1.9 of the induction up in such a way that case distinction on @{term bs} makes
1.10 sense and solves the proof. Part~\ref{Isar} shows you how to write readable
1.11 and stable proofs.