doc-src/Ref/theory-syntax.tex
changeset 9695 ec7d7f877712
parent 6669 5f1ce866c497
     1.1 --- a/doc-src/Ref/theory-syntax.tex	Mon Aug 28 13:50:24 2000 +0200
     1.2 +++ b/doc-src/Ref/theory-syntax.tex	Mon Aug 28 13:52:38 2000 +0200
     1.3 @@ -5,10 +5,10 @@
     1.4  
     1.5  \chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}
     1.6  
     1.7 -Below we present the full syntax of theory definition files as
     1.8 -provided by {\Pure} Isabelle --- object-logics may add their own
     1.9 -sections.  \S\ref{sec:ref-defining-theories} explains the meanings of
    1.10 -these constructs.  The syntax obeys the following conventions:
    1.11 +Below we present the full syntax of theory definition files as provided by
    1.12 +Pure Isabelle --- object-logics may add their own sections.
    1.13 +\S\ref{sec:ref-defining-theories} explains the meanings of these constructs.
    1.14 +The syntax obeys the following conventions:
    1.15  \begin{itemize}
    1.16  \item {\tt Typewriter font} denotes terminal symbols.
    1.17