equal
deleted
inserted
replaced
441 the delimiter is preceded by a space and followed by a space or line break; |
441 the delimiter is preceded by a space and followed by a space or line break; |
442 the entire phrase is a pretty printing block. |
442 the entire phrase is a pretty printing block. |
443 |
443 |
444 The alternative notation \<^verbatim>\<open>(\<close>\<open>sy\<close>\<^verbatim>\<open>)\<close> is introduced in addition. Thus any |
444 The alternative notation \<^verbatim>\<open>(\<close>\<open>sy\<close>\<^verbatim>\<open>)\<close> is introduced in addition. Thus any |
445 infix operator may be written in prefix form (as in Haskell), independently of |
445 infix operator may be written in prefix form (as in Haskell), independently of |
446 the number of arguments in the term. To avoid conflict with the comment brackets |
446 the number of arguments. |
447 \<^verbatim>\<open>(*\<close> and \<^verbatim>\<open>*)\<close>, infix operators that begin or end with a \<^verbatim>\<open>*\<close> require |
|
448 extra spaces, e.g. \<^verbatim>\<open>( * )\<close>. |
|
449 \<close> |
447 \<close> |
450 |
448 |
451 |
449 |
452 subsection \<open>Binders\<close> |
450 subsection \<open>Binders\<close> |
453 |
451 |