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