src/Doc/Isar_Ref/Inner_Syntax.thy
changeset 69067 5ed7206dbf18
parent 69065 440f7a575760
child 69580 6f755e3cd95d
equal deleted inserted replaced
69063:765ff343a7aa 69067:5ed7206dbf18
   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