doc-src/IsarRef/pure.tex
changeset 8664 aa383eeb3359
parent 8632 14a69a0e8679
child 8682 82ebf8618e6b
equal deleted inserted replaced
8663:38d7ec8ef683 8664:aa383eeb3359
   848 visible within the logic as actual equations, while abbreviations disappear
   848 visible within the logic as actual equations, while abbreviations disappear
   849 during the input process just after type checking.  Also note that $\DEFNAME$
   849 during the input process just after type checking.  Also note that $\DEFNAME$
   850 does not support polymorphism.
   850 does not support polymorphism.
   851 
   851 
   852 \begin{rail}
   852 \begin{rail}
   853   'let' ((term + 'as') '=' term comment? + 'and')
   853   'let' ((term + 'and') '=' term comment? + 'and')
   854   ;  
   854   ;  
   855 \end{rail}
   855 \end{rail}
   856 
   856 
   857 The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or
   857 The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or
   858 \railnonterm{proppat} (see \S\ref{sec:term-pats}).
   858 \railnonterm{proppat} (see \S\ref{sec:term-pats}).