1.1 --- a/doc-src/TutorialI/Datatype/ABexpr.thy	Fri Aug 04 23:02:11 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Sun Aug 06 15:26:53 2000 +0200
     1.3 @@ -113,7 +113,7 @@
     1.4  \end{ttbox}
     1.5  
     1.6  \begin{exercise}
     1.7 -  Define a function \isa{norma} of type \isa{'a aexp \isasymFun\ 'a aexp} that
     1.8 +  Define a function \isa{norma} of type @{typ"'a aexp => 'a aexp"} that
     1.9    replaces \isa{IF}s with complex boolean conditions by nested
    1.10    \isa{IF}s where each condition is a \isa{Less} --- \isa{And} and
    1.11    \isa{Neg} should be eliminated completely. Prove that \isa{norma}