--- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,6 +1,6 @@
\begin{isabelle}%
-\isacommand{datatype}~('a,'b){"}term{"}~=~Var~'a~|~App~'b~{"}('a,'b)term\_list{"}\isanewline
-\isakeyword{and}~('a,'b)term\_list~=~Nil~|~Cons~{"}('a,'b)term{"}~{"}('a,'b)term\_list{"}\end{isabelle}%
+\isacommand{datatype}\ ('a,'b){"}term{"}\ =\ Var\ 'a\ |\ App\ 'b\ {"}('a,'b)term\_list{"}\isanewline
+\isakeyword{and}\ ('a,'b)term\_list\ =\ Nil\ |\ Cons\ {"}('a,'b)term{"}\ {"}('a,'b)term\_list{"}\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"