summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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.%