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