doc-src/Ref/defining.tex

                 ~~$|$~~ {\tt\ttlbrace} $id$ {\tt,} \dots {\tt,} $id$ {\tt\ttrbrace}
 \end{tabular}
 \index{*PROP symbol}
 \index{*== symbol}\index{*=?= symbol}\index{*==> symbol}
 \index{*:: symbol}\index{*=> symbol}
-%index command: percent is permitted, but braces must match!
+\index{sort constraints}
+%the index command: a percent is permitted, but braces must match!
 \index{%@{\tt\%} symbol}
 \index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
 \index{*[ symbol}\index{*] symbol}
 \index{*"!"! symbol}
 \index{*"["| symbol}

 \begin{warn}
   In {\tt idts}, note that \verb|x::nat y| is parsed as \verb|x::(nat y)|,
   treating {\tt y} like a type constructor applied to {\tt nat}.  The
   likely result is an error message.  To avoid this interpretation, use
   parentheses and write \verb|(x::nat) y|.
+  \index{type constraints}\index{*:: symbol}
 
   Similarly, \verb|x::nat y::nat| is parsed as \verb|x::(nat y::nat)| and
   yields an error.  The correct form is \verb|(x::nat) (y::nat)|.
 \end{warn}
 

 {\out print_translation: "all"}
 {\out print_rules:}
 {\out print_ast_translation: "==>" "_abs" "_idts" "fun"}
 \end{ttbox}
 
-As you can see, the output is divided into labeled sections.  The grammar
+As you can see, the output is divided into labelled sections.  The grammar
 is represented by {\tt lexicon}, {\tt roots} and {\tt prods}.  The rest
 refers to syntactic translations and macro expansion.  Here is an
 explanation of the various sections.
 \begin{description}
   \item[{\tt lexicon}] lists the delimiters used for lexical

 
 A simple type is typically declared for each nonterminal symbol.  In
 first-order logic, type~$i$ stands for terms and~$o$ for formulae.  Only
 the outermost type constructor is taken into account.  For example, any
 type of the form $\sigma list$ stands for a list;  productions may refer
-to the symbol {\tt list} and will apply lists of any type.
+to the symbol {\tt list} and will apply to lists of any type.
 
 The symbol associated with a type is called its {\bf root} since it may
 serve as the root of a parse tree.  Precisely, the root of $(\tau@1, \dots,
 \tau@n)ty$ is $ty$, where $\tau@1$, \ldots, $\tau@n$ are types and $ty$ is
 a type constructor.  Type infixes are a special case of this; in

 Here is a detailed account of mixfix declarations.  Suppose the following
 line occurs within the {\tt consts} section of a {\tt .thy} file:
 \begin{center}
   {\tt $c$ ::\ "$\sigma$" ("$template$" $ps$ $p$)}
 \end{center}
-This constant declaration and mixfix annotation is interpreted as follows:
+This constant declaration and mixfix annotation are interpreted as follows:
 \begin{itemize}\index{productions}
 \item The string {\tt $c$} is the name of the constant associated with the
   production; unless it is a valid identifier, it must be enclosed in
   quotes.  If $c$ is empty (given as~{\tt ""}) then this is a copy
   production.\index{productions!copy} Otherwise, parsing an instance of the

   "*" :: "[exp, exp] => exp"  ("_ * _"  [3, 2] 2)
   "-" :: "exp => exp"         ("- _"    [3] 3)
 end
 \end{ttbox}
 The {\tt arities} declaration causes {\tt exp} to be added as a new root.
-If you put this into a file {\tt exp.thy} and load it via {\tt
+If you put this into a file {\tt EXP.thy} and load it via {\tt
   use_thy "EXP"}, you can run some tests:
 \begin{ttbox}
 val read_exp = Syntax.test_read (syn_of EXP.thy) "exp";
 {\out val it = fn : string -> unit}
 read_exp "0 * 0 * 0 * 0 + 0 + 0 + 0";

 \begin{ttbox}
 \(c\)    :: "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)"
 "\(\Q\)"\hskip-3pt  :: "[idts, \(\tau@2\)] => \(\tau@3\)"   ("(3\(\Q\)_./ _)" \(p\))
 \end{ttbox}
 Here \ndx{idts} is the nonterminal symbol for a list of identifiers with
+\index{type constraints}
 optional type constraints (see Fig.\ts\ref{fig:pure_gram}).  The
 declaration also installs a parse translation\index{translations!parse}
 for~$\Q$ and a print translation\index{translations!print} for~$c$ to
 translate between the internal and external forms.
 

 consts
   Trueprop :: "o => prop"   ("_" 5)
 end
 \end{ttbox}
 The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible
-coercion function.  Assuming this definition resides in a file {\tt base.thy},
+coercion function.  Assuming this definition resides in a file {\tt Base.thy},
 you have to load it with the command {\tt use_thy "Base"}.
 
 One of the simplest nontrivial logics is {\bf minimal logic} of
 implication.  Its definition in Isabelle needs no advanced features but
 illustrates the overall mechanism nicely:

   K     "P --> Q --> P"
   S     "(P --> Q --> R) --> (P --> Q) --> P --> R"
   MP    "[| P --> Q; P |] ==> Q"
 end
 \end{ttbox}
-After loading this definition from the file {\tt hilbert.thy}, you can
+After loading this definition from the file {\tt Hilbert.thy}, you can
 start to prove theorems in the logic:
 \begin{ttbox}
 goal Hilbert.thy "P --> P";
 {\out Level 0}
 {\out P --> P}