equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 % |
3 % |
3 \begin{isamarkuptext}% |
4 \begin{isamarkuptext}% |
4 To minimize running time, each node of a trie should contain an array that maps |
5 To minimize running time, each node of a trie should contain an array that maps |
5 letters to subtries. We have chosen a (sometimes) more space efficient |
6 letters to subtries. We have chosen a (sometimes) more space efficient |
6 representation where the subtries are held in an association list, i.e.\ a |
7 representation where the subtries are held in an association list, i.e.\ a |
120 brittle) magic of \isa{auto} (\isa{simp\_all} will not do---try it) to split the subgoals |
121 brittle) magic of \isa{auto} (\isa{simp\_all} will not do---try it) to split the subgoals |
121 of the induction up in such a way that case distinction on \isa{bs} makes sense and |
122 of the induction up in such a way that case distinction on \isa{bs} makes sense and |
122 solves the proof. Part~\ref{Isar} shows you how to write readable and stable |
123 solves the proof. Part~\ref{Isar} shows you how to write readable and stable |
123 proofs.% |
124 proofs.% |
124 \end{isamarkuptext}% |
125 \end{isamarkuptext}% |
125 \end{isabelle}% |
126 \end{isabellebody}% |
126 %%% Local Variables: |
127 %%% Local Variables: |
127 %%% mode: latex |
128 %%% mode: latex |
128 %%% TeX-master: "root" |
129 %%% TeX-master: "root" |
129 %%% End: |
130 %%% End: |