equal
deleted
inserted
replaced
7 \endisadelimtheory |
7 \endisadelimtheory |
8 % |
8 % |
9 \isatagtheory |
9 \isatagtheory |
10 \isacommand{theory}\isamarkupfalse% |
10 \isacommand{theory}\isamarkupfalse% |
11 \ ToyList\isanewline |
11 \ ToyList\isanewline |
12 \isakeyword{imports}\ PreList\isanewline |
12 \isakeyword{imports}\ Datatype\isanewline |
13 \isakeyword{begin}% |
13 \isakeyword{begin}% |
14 \endisatagtheory |
14 \endisatagtheory |
15 {\isafoldtheory}% |
15 {\isafoldtheory}% |
16 % |
16 % |
17 \isadelimtheory |
17 \isadelimtheory |
21 \begin{isamarkuptext}% |
21 \begin{isamarkuptext}% |
22 \noindent |
22 \noindent |
23 HOL already has a predefined theory of lists called \isa{List} --- |
23 HOL already has a predefined theory of lists called \isa{List} --- |
24 \isa{ToyList} is merely a small fragment of it chosen as an example. In |
24 \isa{ToyList} is merely a small fragment of it chosen as an example. In |
25 contrast to what is recommended in \S\ref{sec:Basic:Theories}, |
25 contrast to what is recommended in \S\ref{sec:Basic:Theories}, |
26 \isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a |
26 \isa{ToyList} is not based on \isa{Main} but on \isa{Datatype}, a |
27 theory that contains pretty much everything but lists, thus avoiding |
27 theory that contains pretty much everything but lists, thus avoiding |
28 ambiguities caused by defining lists twice.% |
28 ambiguities caused by defining lists twice.% |
29 \end{isamarkuptext}% |
29 \end{isamarkuptext}% |
30 \isamarkuptrue% |
30 \isamarkuptrue% |
31 \isacommand{datatype}\isamarkupfalse% |
31 \isacommand{datatype}\isamarkupfalse% |