equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 \isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}% |
3 \isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}% |
3 \begin{isamarkuptext}% |
4 \begin{isamarkuptext}% |
4 \noindent |
5 \noindent |
5 HOL already has a predefined theory of lists called \isa{List} --- |
6 HOL already has a predefined theory of lists called \isa{List} --- |
6 \isa{ToyList} is merely a small fragment of it chosen as an example. In |
7 \isa{ToyList} is merely a small fragment of it chosen as an example. In |
322 \noindent |
323 \noindent |
323 The final \isa{end} tells Isabelle to close the current theory because |
324 The final \isa{end} tells Isabelle to close the current theory because |
324 we are finished with its development:% |
325 we are finished with its development:% |
325 \end{isamarkuptext}% |
326 \end{isamarkuptext}% |
326 \isacommand{end}\isanewline |
327 \isacommand{end}\isanewline |
327 \end{isabelle}% |
328 \end{isabellebody}% |
328 %%% Local Variables: |
329 %%% Local Variables: |
329 %%% mode: latex |
330 %%% mode: latex |
330 %%% TeX-master: "root" |
331 %%% TeX-master: "root" |
331 %%% End: |
332 %%% End: |