1.1 --- a/doc-src/Ref/defining.tex	Fri Oct 10 19:34:28 2003 +0200
     1.2 +++ b/doc-src/Ref/defining.tex	Mon Oct 13 16:54:20 2003 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  The syntax of an Isabelle logic is specified by a {\bf priority
     1.5    grammar}.\index{priorities} Each nonterminal is decorated by an integer
     1.6  priority, as in~$A^{(p)}$.  A nonterminal $A^{(p)}$ in a derivation may be
     1.7 -rewritten using a production $A^{(q)} = \gamma$ only if~$p \le q$.  Any
     1.8 +rewritten using a production $A^{(q)} = \gamma$ only if~$p \leq q$.  Any
     1.9  priority grammar can be translated into a normal context free grammar by
    1.10  introducing new nonterminals and productions.
    1.11  
    1.12 @@ -40,7 +40,7 @@
    1.13  relation $\longrightarrow@G$.  Let $\alpha$ and $\beta$ denote strings of
    1.14  terminal or nonterminal symbols.  Then
    1.15  \[ \alpha\, A^{(p)}\, \beta ~\longrightarrow@G~ \alpha\,\gamma\,\beta \]
    1.16 -if and only if $G$ contains some production $A^{(q)}=\gamma$ for~$p \le q$.
    1.17 +if and only if $G$ contains some production $A^{(q)}=\gamma$ for~$p \leq q$.
    1.18  
    1.19  The following simple grammar for arithmetic expressions demonstrates how
    1.20  binding power and associativity of operators can be enforced by priorities.
    1.21 @@ -172,7 +172,7 @@
    1.22      
    1.23    \item[\ndxbold{pttrn}, \ndxbold{pttrns}] denote patterns for
    1.24      abstraction, cases etc.  Initially the same as $idt$ and $idts$,
    1.25 -    these are indetended to be augmented by user extensions.
    1.26 +    these are intended to be augmented by user extensions.
    1.27  
    1.28    \item[\ndxbold{type}] denotes types of the meta-logic.
    1.29