1.1 --- a/doc-src/IsarRef/conversion.tex	Fri Mar 08 15:33:32 2002 +0100
     1.2 +++ b/doc-src/IsarRef/conversion.tex	Fri Mar 08 15:53:15 2002 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4  
     1.5 -\chapter{Isabelle/Isar Conversion Guide}\label{ap:conv}
     1.6 +\chapter{Isabelle/Isar conversion guide}\label{ap:conv}
     1.7  
     1.8  Subsequently, we give a few practical hints on working in a mixed environment
     1.9  of old Isabelle ML proof scripts and new Isabelle/Isar theories.  There are
    1.10 @@ -39,21 +39,21 @@
    1.11  \begin{descr}
    1.12  \item [$\mathtt{thm}~name$ and $\mathtt{thms}~name$] retrieve theorems stored
    1.13    in the current theory context, including any ancestor node.
    1.14 -  
    1.15 +
    1.16    The convention of old-style theories was to bind any theorem as an ML value
    1.17    as well.  New-style theories no longer do this, so ML code may require
    1.18    \texttt{thm~"foo"} rather than just \texttt{foo}.
    1.19 -  
    1.20 +
    1.21  \item [$\mathtt{the_context()}$] refers to the current theory context.
    1.22 -  
    1.23 +
    1.24    Old-style theories often use the ML binding \texttt{thy}, which is
    1.25    dynamically created by the ML code generated from old theory source.  This
    1.26    is no longer the recommended way in any case!  Function \texttt{the_context}
    1.27    should be used for old scripts as well.
    1.28 -  
    1.29 +
    1.30  \item [$\mathtt{theory}~name$] retrieves the named theory from the global
    1.31    theory-loader database.
    1.32 -  
    1.33 +
    1.34    The ML code generated from old-style theories would include an ML binding
    1.35    $name\mathtt{.thy}$ as part of an ML structure.
    1.36  \end{descr}
    1.37 @@ -72,11 +72,11 @@
    1.38  these later.
    1.39  
    1.40  \begin{descr}
    1.41 -  
    1.42 +
    1.43  \item [$\mathtt{qed}~name$] is the canonical way to conclude a proof script in
    1.44    ML.  This already manages entry in the theorem database of the current
    1.45    theory context.
    1.46 -  
    1.47 +
    1.48  \item [$\mathtt{bind_thm}~(name, thm)$ and $\mathtt{bind_thms}~(name, thms)$]
    1.49    store theorems that have been produced in ML in an ad-hoc manner.
    1.50  
    1.51 @@ -133,13 +133,13 @@
    1.52  \item Quoted strings may contain arbitrary white space, and span several lines
    1.53    without requiring \verb,\,\,\dots\verb,\, escapes.
    1.54  \item Names may always be quoted.
    1.55 -  
    1.56 +
    1.57    The old syntax would occasionally demand plain identifiers vs.\ quoted
    1.58    strings to accommodate certain syntactic features.
    1.59  \item Types and terms have to be \emph{atomic} as far as the theory syntax is
    1.60    concerned; this typically requires quoting of input strings, e.g.\ ``$x +
    1.61    y$''.
    1.62 -  
    1.63 +
    1.64    The old theory syntax used to fake part of the syntax of types in order to
    1.65    require less quoting in common cases; this was hard to predict, though.  On
    1.66    the other hand, Isar does not require quotes for simple terms, such as plain
    1.67 @@ -300,12 +300,12 @@
    1.68  rule applications (based on higher-order resolution).  The space of resolution
    1.69  tactics has the following main dimensions.
    1.70  \begin{enumerate}
    1.71 -\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\ 
    1.72 +\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\
    1.73    \texttt{resolve_tac}, \texttt{eresolve_tac}, \texttt{dresolve_tac},
    1.74    \texttt{forward_tac}).
    1.75 -\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\ 
    1.76 +\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\
    1.77    \texttt{res_inst_tac}).
    1.78 -\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\ 
    1.79 +\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\
    1.80    \texttt{rtac}).
    1.81  \end{enumerate}
    1.82  
    1.83 @@ -348,9 +348,9 @@
    1.84  
    1.85  The main Simplifier tactics \texttt{Simp_tac}, \texttt{simp_tac} and variants
    1.86  (cf.\ \cite{isabelle-ref}) are all covered by the $simp$ and $simp_all$
    1.87 -methods (see \S\ref{sec:simp}).  Note that there is no individual goal
    1.88 -addressing available, simplification acts either on the first goal ($simp$)
    1.89 -or all goals ($simp_all$).
    1.90 +methods (see \S\ref{sec:simplifier}).  Note that there is no individual goal
    1.91 +addressing available, simplification acts either on the first goal ($simp$) or
    1.92 +all goals ($simp_all$).
    1.93  
    1.94  \begin{matharray}{lll}
    1.95    \texttt{Asm_full_simp_tac 1} & & simp \\
    1.96 @@ -361,8 +361,9 @@
    1.97  \end{matharray}
    1.98  
    1.99  Isar also provides separate method modifier syntax for augmenting the
   1.100 -Simplifier context (see \S\ref{sec:simp}), which is known as the ``simpset''
   1.101 -in ML.  A typical ML expression with simpset changes looks like this:
   1.102 +Simplifier context (see \S\ref{sec:simplifier}), which is known as the
   1.103 +``simpset'' in ML.  A typical ML expression with simpset changes looks like
   1.104 +this:
   1.105  \begin{ttbox}
   1.106  asm_full_simp_tac (simpset () addsimps [\(a@1\), \(\dots\)] delsimps [\(b@1\), \(\dots\)]) 1
   1.107  \end{ttbox}
   1.108 @@ -380,7 +381,7 @@
   1.109  automated tactics, such as \texttt{Blast_tac}, \texttt{Fast_tac},
   1.110  \texttt{Clarify_tac} etc.\ (see \cite{isabelle-ref}).  The corresponding Isar
   1.111  methods usually share the same base name, such as $blast$, $fast$, $clarify$
   1.112 -etc.\ (see \S\ref{sec:classical-auto}).
   1.113 +etc.\ (see \S\ref{sec:classical}).
   1.114  
   1.115  Similar to the Simplifier, there is separate method modifier syntax for
   1.116  augmenting the Classical Reasoner context, which is known as the ``claset'' in
   1.117 @@ -442,14 +443,13 @@
   1.118  \medskip \texttt{ALLGOALS}, \texttt{SOMEGOAL} etc.\ (see \cite{isabelle-ref})
   1.119  are not available in Isar, since there is no direct goal addressing.
   1.120  Nevertheless, some basic methods address all goals internally, notably
   1.121 -$simp_all$ (see \S\ref{sec:simp}).  Also note that \texttt{ALLGOALS} may be
   1.122 -often replaced by ``$+$'' (repeat at least once), although this usually has a
   1.123 -different operational behavior, such as solving goals in a different order.
   1.124 +$simp_all$ (see \S\ref{sec:simplifier}).  Also note that \texttt{ALLGOALS} may
   1.125 +be often replaced by ``$+$'' (repeat at least once), although this usually has
   1.126 +a different operational behavior, such as solving goals in a different order.
   1.127  
   1.128  \medskip Iterated resolution, such as
   1.129  \texttt{REPEAT~(FIRSTGOAL~(resolve_tac~$\dots$))}, is usually better expressed
   1.130 -using the $intro$ and $elim$ methods of Isar (see
   1.131 -\S\ref{sec:classical-basic}).
   1.132 +using the $intro$ and $elim$ methods of Isar (see \S\ref{sec:classical}).
   1.133  
   1.134  
   1.135  \subsection{Declarations and ad-hoc operations}\label{sec:conv-decls}
   1.136 @@ -559,8 +559,7 @@
   1.137  machine-checked formal proof.  Depending on the context of application, this
   1.138  might be even indispensable to start with!
   1.139  
   1.140 -
   1.141 -%%% Local Variables: 
   1.142 +%%% Local Variables:
   1.143  %%% mode: latex
   1.144  %%% TeX-master: "isar-ref"
   1.145 -%%% End: 
   1.146 +%%% End:

     2.1 --- a/doc-src/IsarRef/generic.tex	Fri Mar 08 15:33:32 2002 +0100
     2.2 +++ b/doc-src/IsarRef/generic.tex	Fri Mar 08 15:53:15 2002 +0100
     2.3 @@ -1,5 +1,5 @@
     2.4  
     2.5 -\chapter{Generic Tools and Packages}\label{ch:gen-tools}
     2.6 +\chapter{Generic tools and packages}\label{ch:gen-tools}
     2.7  
     2.8  \section{Theory specification commands}
     2.9  
    2.10 @@ -62,6 +62,7 @@
    2.11  that are modeled after the Isar proof context commands (cf.\
    2.12  \S\ref{sec:proof-context}).
    2.13  
    2.14 +
    2.15  \subsubsection{Localized commands}
    2.16  
    2.17  Existing locales may be augmented later on by adding new facts.  Note that the
    2.18 @@ -238,10 +239,9 @@
    2.19  \end{matharray}
    2.20  
    2.21  Typically, the soundness proof is relatively straight-forward, often just by
    2.22 -canonical automated tools such as ``$\BY{simp}$'' (see \S\ref{sec:simp}) or
    2.23 -``$\BY{blast}$'' (see \S\ref{sec:classical-auto}).  Accordingly, the
    2.24 -``$that$'' reduction above is declared as simplification and introduction
    2.25 -rule.
    2.26 +canonical automated tools such as ``$\BY{simp}$'' or ``$\BY{blast}$''.
    2.27 +Accordingly, the ``$that$'' reduction above is declared as simplification and
    2.28 +introduction rule.
    2.29  
    2.30  \medskip
    2.31  
    2.32 @@ -466,9 +466,9 @@
    2.33  \item [$elim_format$] turns a destruction rule into elimination rule format,
    2.34    by resolving with the rule $\PROP A \Imp (\PROP A \Imp \PROP B) \Imp \PROP
    2.35    B$.
    2.36 -
    2.37 -  Note that the Classical Reasoner (\S\ref{sec:classical-att}) provides its
    2.38 -  own version of this operation.
    2.39 +  
    2.40 +  Note that the Classical Reasoner (\S\ref{sec:classical}) provides its own
    2.41 +  version of this operation.
    2.42  
    2.43  \item [$standard$] puts a theorem into the standard form of object-rules at
    2.44    the outermost theory level.  Note that this operation violates the local
    2.45 @@ -612,7 +612,7 @@
    2.46  
    2.47  \subsection{The Simplifier}\label{sec:simplifier}
    2.48  
    2.49 -\subsubsection{Simplification methods}\label{sec:simp}
    2.50 +\subsubsection{Simplification methods}
    2.51  
    2.52  \indexisarmeth{simp}\indexisarmeth{simp-all}
    2.53  \begin{matharray}{rcl}
    2.54 @@ -737,13 +737,12 @@
    2.55  \end{rail}
    2.56  
    2.57  \begin{descr}
    2.58 -
    2.59 +  
    2.60  \item [$simplified~\vec a$] causes a theorem to be simplified, either by
    2.61    exactly the specified rules $\vec a$, or the implicit Simplifier context if
    2.62    no arguments are given.  The result is fully simplified by default,
    2.63    including assumptions and conclusion; the options $no_asm$ etc.\ tune the
    2.64 -  Simplifier in the same way as the for the $simp$ method (see
    2.65 -  \S\ref{sec:simp}).
    2.66 +  Simplifier in the same way as the for the $simp$ method.
    2.67  
    2.68    Note that forward simplification restricts the simplifier to its most basic
    2.69    operation of term rewriting; solver and looper tactics \cite{isabelle-ref}
    2.70 @@ -753,7 +752,7 @@
    2.71  \end{descr}
    2.72  
    2.73  
    2.74 -\subsubsection{Low-level equational reasoning}\label{sec:basic-eq}
    2.75 +\subsubsection{Low-level equational reasoning}
    2.76  
    2.77  \indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}
    2.78  \begin{matharray}{rcl}
    2.79 @@ -787,15 +786,15 @@
    2.80  \item [$split~\vec a$] performs single-step case splitting using rules $thms$.
    2.81    By default, splitting is performed in the conclusion of a goal; the $asm$
    2.82    option indicates to operate on assumptions instead.
    2.83 -
    2.84 +  
    2.85    Note that the $simp$ method already involves repeated application of split
    2.86 -  rules as declared in the current context (see \S\ref{sec:simp}).
    2.87 +  rules as declared in the current context.
    2.88  \end{descr}
    2.89  
    2.90  
    2.91  \subsection{The Classical Reasoner}\label{sec:classical}
    2.92  
    2.93 -\subsubsection{Basic methods}\label{sec:classical-basic}
    2.94 +\subsubsection{Basic methods}
    2.95  
    2.96  \indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
    2.97  \indexisarmeth{intro}\indexisarmeth{elim}
    2.98 @@ -835,7 +834,7 @@
    2.99  \end{descr}
   2.100  
   2.101  
   2.102 -\subsubsection{Automated methods}\label{sec:classical-auto}
   2.103 +\subsubsection{Automated methods}
   2.104  
   2.105  \indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow}
   2.106  \indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify}
   2.107 @@ -908,9 +907,9 @@
   2.108    tactics.  These correspond to \texttt{auto_tac}, \texttt{force_tac},
   2.109    \texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
   2.110    added as wrapper, see \cite[\S11]{isabelle-ref} for more information.  The
   2.111 -  modifier arguments correspond to those given in \S\ref{sec:simp} and
   2.112 -  \S\ref{sec:classical-auto}.  Just note that the ones related to the
   2.113 -  Simplifier are prefixed by \railtterm{simp} here.
   2.114 +  modifier arguments correspond to those given in \S\ref{sec:simplifier} and
   2.115 +  \S\ref{sec:classical}.  Just note that the ones related to the Simplifier
   2.116 +  are prefixed by \railtterm{simp} here.
   2.117  
   2.118    Facts provided by forward chaining are inserted into the goal before doing
   2.119    the search.  The ``!''~argument causes the full context of assumptions to be
   2.120 @@ -918,7 +917,7 @@
   2.121  \end{descr}
   2.122  
   2.123  
   2.124 -\subsubsection{Declaring rules}\label{sec:classical-mod}
   2.125 +\subsubsection{Declaring rules}
   2.126  
   2.127  \indexisarcmd{print-claset}
   2.128  \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
   2.129 @@ -969,7 +968,7 @@
   2.130  \end{descr}
   2.131  
   2.132  
   2.133 -\subsubsection{Classical operations}\label{sec:classical-att}
   2.134 +\subsubsection{Classical operations}
   2.135  
   2.136  \indexisaratt{elim-format}\indexisaratt{swapped}
   2.137  
   2.138 @@ -994,7 +993,7 @@
   2.139  
   2.140  \subsection{Proof by cases and induction}\label{sec:cases-induct}
   2.141  
   2.142 -\subsubsection{Rule contexts}\label{sec:rule-cases}
   2.143 +\subsubsection{Rule contexts}
   2.144  
   2.145  \indexisarcmd{case}\indexisarcmd{print-cases}
   2.146  \indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes}
   2.147 @@ -1106,9 +1105,9 @@
   2.148  and induction over datatypes, inductive sets, and recursive functions.  The
   2.149  corresponding rules may be specified and instantiated in a casual manner.
   2.150  Furthermore, these methods provide named local contexts that may be invoked
   2.151 -via the $\CASENAME$ proof command within the subsequent proof text (cf.\
   2.152 -\S\ref{sec:rule-cases}).  This accommodates compact proof texts even when
   2.153 -reasoning about large specifications.
   2.154 +via the $\CASENAME$ proof command within the subsequent proof text.  This
   2.155 +accommodates compact proof texts even when reasoning about large
   2.156 +specifications.
   2.157  
   2.158  \begin{rail}
   2.159    'cases' spec
   2.160 @@ -1175,16 +1174,16 @@
   2.161  
   2.162  \end{descr}
   2.163  
   2.164 -Above methods produce named local contexts (cf.\ \S\ref{sec:rule-cases}), as
   2.165 -determined by the instantiated rule as specified in the text.  Beyond that,
   2.166 -the $induct$ method guesses further instantiations from the goal specification
   2.167 -itself.  Any persisting unresolved schematic variables of the resulting rule
   2.168 -will render the the corresponding case invalid.  The term binding
   2.169 -$\Var{case}$\indexisarvar{case} for the conclusion will be provided with each
   2.170 -case, provided that term is fully specified.
   2.171 +Above methods produce named local contexts, as determined by the instantiated
   2.172 +rule as specified in the text.  Beyond that, the $induct$ method guesses
   2.173 +further instantiations from the goal specification itself.  Any persisting
   2.174 +unresolved schematic variables of the resulting rule will render the the
   2.175 +corresponding case invalid.  The term binding $\Var{case}$\indexisarvar{case}
   2.176 +for the conclusion will be provided with each case, provided that term is
   2.177 +fully specified.
   2.178  
   2.179 -The $\isarkeyword{print_cases}$ command (\S\ref{sec:rule-cases}) prints all
   2.180 -named cases present in the current proof state.
   2.181 +The $\isarkeyword{print_cases}$ command prints all named cases present in the
   2.182 +current proof state.
   2.183  
   2.184  \medskip
   2.185  
   2.186 @@ -1242,10 +1241,10 @@
   2.187    corresponding methods of the same name.  Certain definitional packages of
   2.188    object-logics usually declare emerging cases and induction rules as
   2.189    expected, so users rarely need to intervene.
   2.190 -
   2.191 +  
   2.192    Manual rule declarations usually include the the $case_names$ and $ps$
   2.193    attributes to adjust names of cases and parameters of a rule (see
   2.194 -  \S\ref{sec:rule-cases}); the $consumes$ declaration is taken care of
   2.195 +  \S\ref{sec:cases-induct}); the $consumes$ declaration is taken care of
   2.196    automatically: $consumes~0$ is specified for ``type'' rules and $consumes~1$
   2.197    for ``set'' rules.
   2.198  

     3.1 --- a/doc-src/IsarRef/isar-ref.tex	Fri Mar 08 15:33:32 2002 +0100
     3.2 +++ b/doc-src/IsarRef/isar-ref.tex	Fri Mar 08 15:53:15 2002 +0100
     3.3 @@ -24,25 +24,25 @@
     3.4  \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
     3.5  \railterm{name,nameref,text,type,term,prop,atom}
     3.6  
     3.7 -\railalias{ident}{\railtoken{ident}}
     3.8 -\railalias{longident}{\railtoken{longident}}
     3.9 -\railalias{symident}{\railtoken{symident}}
    3.10 -\railalias{var}{\railtoken{var}}
    3.11 -\railalias{textvar}{\railtoken{textvar}}
    3.12 -\railalias{typefree}{\railtoken{typefree}}
    3.13 -\railalias{typevar}{\railtoken{typevar}}
    3.14 -\railalias{nat}{\railtoken{nat}}
    3.15 -\railalias{string}{\railtoken{string}}
    3.16 -\railalias{verbatim}{\railtoken{verbatim}}
    3.17 -\railalias{keyword}{\railtoken{keyword}}
    3.18 +\railalias{ident}{\railtok{ident}}
    3.19 +\railalias{longident}{\railtok{longident}}
    3.20 +\railalias{symident}{\railtok{symident}}
    3.21 +\railalias{var}{\railtok{var}}
    3.22 +\railalias{textvar}{\railtok{textvar}}
    3.23 +\railalias{typefree}{\railtok{typefree}}
    3.24 +\railalias{typevar}{\railtok{typevar}}
    3.25 +\railalias{nat}{\railtok{nat}}
    3.26 +\railalias{string}{\railtok{string}}
    3.27 +\railalias{verbatim}{\railtok{verbatim}}
    3.28 +\railalias{keyword}{\railtok{keyword}}
    3.29  
    3.30 -\railalias{name}{\railqtoken{name}}
    3.31 -\railalias{nameref}{\railqtoken{nameref}}
    3.32 -\railalias{text}{\railqtoken{text}}
    3.33 -\railalias{type}{\railqtoken{type}}
    3.34 -\railalias{term}{\railqtoken{term}}
    3.35 -\railalias{prop}{\railqtoken{prop}}
    3.36 -\railalias{atom}{\railqtoken{atom}}
    3.37 +\railalias{name}{\railqtok{name}}
    3.38 +\railalias{nameref}{\railqtok{nameref}}
    3.39 +\railalias{text}{\railqtok{text}}
    3.40 +\railalias{type}{\railqtok{type}}
    3.41 +\railalias{term}{\railqtok{term}}
    3.42 +\railalias{prop}{\railqtok{prop}}
    3.43 +\railalias{atom}{\railqtok{atom}}
    3.44  
    3.45  \newcommand{\drv}{\mathrel{\vdash}}
    3.46  \newcommand{\edrv}{\mathop{\drv}\nolimits}

     4.1 --- a/doc-src/IsarRef/logics.tex	Fri Mar 08 15:33:32 2002 +0100
     4.2 +++ b/doc-src/IsarRef/logics.tex	Fri Mar 08 15:53:15 2002 +0100
     4.3 @@ -1,5 +1,5 @@
     4.4  
     4.5 -\chapter{Object-logic Specific Elements}\label{ch:logics}
     4.6 +\chapter{Object-logic specific elements}\label{ch:logics}
     4.7  
     4.8  \section{General logic setup}\label{sec:object-logic}
     4.9  

     5.1 --- a/doc-src/IsarRef/pure.tex	Fri Mar 08 15:33:32 2002 +0100
     5.2 +++ b/doc-src/IsarRef/pure.tex	Fri Mar 08 15:53:15 2002 +0100
     5.3 @@ -1,5 +1,5 @@
     5.4  
     5.5 -\chapter{Basic Language Elements}\label{ch:pure-syntax}
     5.6 +\chapter{Basic language elements}\label{ch:pure-syntax}
     5.7  
     5.8  Subsequently, we introduce the main part of Pure theory and proof commands,
     5.9  together with fundamental proof methods and attributes.
    5.10 @@ -508,8 +508,8 @@
    5.11  
    5.12  Syntax translation functions written in ML admit almost arbitrary
    5.13  manipulations of Isabelle's inner syntax.  Any of the above commands have a
    5.14 -single \railqtoken{text} argument that refers to an ML expression of
    5.15 -appropriate type.
    5.16 +single \railqtok{text} argument that refers to an ML expression of appropriate
    5.17 +type.
    5.18  
    5.19  \begin{ttbox}
    5.20  val parse_ast_translation   : (string * (ast list -> ast)) list
    5.21 @@ -837,8 +837,7 @@
    5.22  Any goal statement causes some term abbreviations (such as $\Var{thesis}$) to
    5.23  be bound automatically, see also \S\ref{sec:term-abbrev}.  Furthermore, the
    5.24  local context of a (non-atomic) goal is provided via the
    5.25 -$rule_context$\indexisarcase{rule-context} case, see also
    5.26 -\S\ref{sec:rule-cases}.
    5.27 +$rule_context$\indexisarcase{rule-context} case.
    5.28  
    5.29  \medskip
    5.30  
    5.31 @@ -1042,7 +1041,7 @@
    5.32    the latter will ignore rules declared with ``$?$'', while ``$!$'' are used
    5.33    most aggressively.
    5.34    
    5.35 -  The classical reasoner (see \S\ref{sec:classical-basic}) introduces its own
    5.36 +  The classical reasoner (see \S\ref{sec:classical}) introduces its own
    5.37    variants of these attributes; use qualified names to access the present
    5.38    versions of Isabelle/Pure, i.e.\ $Pure{\dtt}intro$ or $CPure{\dtt}intro$.
    5.39    

     6.1 --- a/doc-src/IsarRef/refcard.tex	Fri Mar 08 15:33:32 2002 +0100
     6.2 +++ b/doc-src/IsarRef/refcard.tex	Fri Mar 08 15:53:15 2002 +0100
     6.3 @@ -1,5 +1,5 @@
     6.4  
     6.5 -\chapter{Isabelle/Isar Quick Reference}\label{ap:refcard}
     6.6 +\chapter{Isabelle/Isar quick reference}\label{ap:refcard}
     6.7  
     6.8  \section{Proof commands}
     6.9  

     7.1 --- a/doc-src/IsarRef/syntax.tex	Fri Mar 08 15:33:32 2002 +0100
     7.2 +++ b/doc-src/IsarRef/syntax.tex	Fri Mar 08 15:53:15 2002 +0100
     7.3 @@ -1,5 +1,5 @@
     7.4  
     7.5 -\chapter{Syntax Primitives}
     7.6 +\chapter{Syntax primitives}
     7.7  
     7.8  The rather generic framework of Isabelle/Isar syntax emerges from three main
     7.9  syntactic categories: \emph{commands} of the top-level Isar engine (covering
    7.10 @@ -130,21 +130,21 @@
    7.11  Isar language elements to be described later.
    7.12  
    7.13  Note that some of the basic syntactic entities introduced below (e.g.\ 
    7.14 -\railqtoken{name}) act much like tokens rather than plain nonterminals (e.g.\ 
    7.15 +\railqtok{name}) act much like tokens rather than plain nonterminals (e.g.\ 
    7.16  \railnonterm{sort}), especially for the sake of error messages.  E.g.\ syntax
    7.17 -elements like $\CONSTS$ referring to \railqtoken{name} or \railqtoken{type}
    7.18 -would really report a missing name or type rather than any of the constituent
    7.19 -primitive tokens such as \railtoken{ident} or \railtoken{string}.
    7.20 +elements like $\CONSTS$ referring to \railqtok{name} or \railqtok{type} would
    7.21 +really report a missing name or type rather than any of the constituent
    7.22 +primitive tokens such as \railtok{ident} or \railtok{string}.
    7.23  
    7.24  
    7.25  \subsection{Names}
    7.26  
    7.27 -Entity \railqtoken{name} usually refers to any name of types, constants,
    7.28 +Entity \railqtok{name} usually refers to any name of types, constants,
    7.29  theorems etc.\ that are to be \emph{declared} or \emph{defined} (so qualified
    7.30  identifiers are excluded here).  Quoted strings provide an escape for
    7.31  non-identifier names or those ruled out by outer syntax keywords (e.g.\ 
    7.32  \verb|"let"|).  Already existing objects are usually referenced by
    7.33 -\railqtoken{nameref}.
    7.34 +\railqtok{nameref}.
    7.35  
    7.36  \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
    7.37  \indexoutertoken{int}
    7.38 @@ -162,12 +162,11 @@
    7.39  
    7.40  \subsection{Comments}\label{sec:comments}
    7.41  
    7.42 -Large chunks of plain \railqtoken{text} are usually given
    7.43 -\railtoken{verbatim}, i.e.\ enclosed in \verb|{*|~\dots~\verb|*}|.  For
    7.44 -convenience, any of the smaller text units conforming to \railqtoken{nameref}
    7.45 -are admitted as well.  A marginal \railnonterm{comment} is of the form
    7.46 -\texttt{--} \railqtoken{text}.  Any number of these may occur within
    7.47 -Isabelle/Isar commands.
    7.48 +Large chunks of plain \railqtok{text} are usually given \railtok{verbatim},
    7.49 +i.e.\ enclosed in \verb|{*|~\dots~\verb|*}|.  For convenience, any of the
    7.50 +smaller text units conforming to \railqtok{nameref} are admitted as well.  A
    7.51 +marginal \railnonterm{comment} is of the form \texttt{--} \railqtok{text}.
    7.52 +Any number of these may occur within Isabelle/Isar commands.
    7.53  
    7.54  \indexoutertoken{text}\indexouternonterm{comment}
    7.55  \begin{rail}
    7.56 @@ -269,7 +268,7 @@
    7.57    ;
    7.58  \end{rail}
    7.59  
    7.60 -Here the \railtoken{string} specifications refer to the actual mixfix template
    7.61 +Here the \railtok{string} specifications refer to the actual mixfix template
    7.62  (see also \cite{isabelle-ref}), which may include literal text, spacing,
    7.63  blocks, and arguments (denoted by ``$_$''); the special symbol \verb,\<index>,
    7.64  (printed as ``\i'') represents an index argument that specifies an implicit
    7.65 @@ -287,7 +286,7 @@
    7.66  ``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternative choices),
    7.67  ``\texttt{?}'' (try), ``\texttt{+}'' (repeat at least once).  In practice,
    7.68  proof methods are usually just a comma separated list of
    7.69 -\railqtoken{nameref}~\railnonterm{args} specifications.  Note that parentheses
    7.70 +\railqtok{nameref}~\railnonterm{args} specifications.  Note that parentheses
    7.71  may be dropped for single method specifications (with no arguments).
    7.72  
    7.73  \indexouternonterm{method}
    7.74 @@ -317,8 +316,8 @@
    7.75  \railnonterm{args} below is parsed by the attribute a second time.  The
    7.76  attribute argument specifications may be any sequence of atomic entities
    7.77  (identifiers, strings etc.), or properly bracketed argument lists.  Below
    7.78 -\railqtoken{atom} refers to any atomic entity, including any
    7.79 -\railtoken{keyword} conforming to \railtoken{symident}.
    7.80 +\railqtok{atom} refers to any atomic entity, including any \railtok{keyword}
    7.81 +conforming to \railtok{symident}.
    7.82  
    7.83  \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
    7.84  \begin{rail}
    7.85 @@ -366,8 +365,8 @@
    7.86  Wherever explicit propositions (or term fragments) occur in a proof text,
    7.87  casual binding of schematic term variables may be given specified via patterns
    7.88  of the form ``$\ISS{p@1\;\dots}{p@n}$''.  There are separate versions
    7.89 -available for \railqtoken{term}s and \railqtoken{prop}s.  The latter provides
    7.90 -a $\CONCLNAME$ part with patterns referring the (atomic) conclusion of a rule.
    7.91 +available for \railqtok{term}s and \railqtok{prop}s.  The latter provides a
    7.92 +$\CONCLNAME$ part with patterns referring the (atomic) conclusion of a rule.
    7.93  
    7.94  \indexouternonterm{termpat}\indexouternonterm{proppat}
    7.95  \begin{rail}

     8.1 --- a/doc-src/railsetup.sty	Fri Mar 08 15:33:32 2002 +0100
     8.2 +++ b/doc-src/railsetup.sty	Fri Mar 08 15:53:15 2002 +0100
     8.3 @@ -27,6 +27,6 @@
     8.4  \def\rail@namefont{\small\rmfamily\itshape}
     8.5  \def\rail@indexfont{\small\rmfamily\itshape}
     8.6  \newcommand{\railtterm}[1]{{\texttt{#1}}}
     8.7 -\newcommand{\railtoken}[1]{{\textrm{#1}}}
     8.8 -\newcommand{\railqtoken}[1]{{\rmfamily\textsl{#1}}}
     8.9 +\newcommand{\railtok}[1]{{\textrm{#1}}}
    8.10 +\newcommand{\railqtok}[1]{{\rmfamily\textsl{#1}}}
    8.11  \newcommand{\railnonterm}[1]{{\emph{#1}}}