doc-src/TutorialI/Datatype/ABexpr.thy
changeset 11309 d666f11ca2d4
parent 10971 6852682eaf16
child 11458 09a6c44a48ea
     1.1 --- a/doc-src/TutorialI/Datatype/ABexpr.thy	Fri May 18 16:45:55 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Fri May 18 17:18:43 2001 +0200
     1.3 @@ -27,8 +27,9 @@
     1.4  
     1.5  text{*\noindent
     1.6  Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler},
     1.7 -except that we have fixed the values to be of type @{typ"nat"} and that we
     1.8 -have fixed the two binary operations @{text Sum} and @{term"Diff"}. Boolean
     1.9 +except that we have added an @{text IF} constructor,
    1.10 +fixed the values to be of type @{typ"nat"} and declared the two binary
    1.11 +operations @{text Sum} and @{term"Diff"}.  Boolean
    1.12  expressions can be arithmetic comparisons, conjunctions and negations.
    1.13  The semantics is fixed via two evaluation functions
    1.14  *}