| author | wenzelm |
| Tue, 18 Jul 2000 14:52:30 +0200 | |
| changeset 9382 | 7cea1cb9703e |
| parent 9145 | 9f7b8de5bfaf |
| child 9541 | d17c0b34d5c8 |
| permissions | -rw-r--r-- |
| 8751 | 1 |
\begin{isabelle}%
|
2 |
\isacommand{datatype}~('a,'b){"}term{"}~=~Var~'a~|~App~'b~{"}('a,'b)term\_list{"}\isanewline
|
|
3 |
\isakeyword{and}~('a,'b)term\_list~=~Nil~|~Cons~{"}('a,'b)term{"}~{"}('a,'b)term\_list{"}\end{isabelle}%
|
|
| 9145 | 4 |
%%% Local Variables: |
5 |
%%% mode: latex |
|
6 |
%%% TeX-master: "root" |
|
7 |
%%% End: |