author wenzelm Thu Mar 07 19:07:56 2002 +0100 (2002-03-07) changeset 13040 02bfd6d622ca parent 13039 cfcc1f6f21df child 13041 6faccf7d0f25
tuned;
     1.1 --- a/doc-src/IsarRef/generic.tex	Thu Mar 07 19:04:00 2002 +0100
1.2 +++ b/doc-src/IsarRef/generic.tex	Thu Mar 07 19:07:56 2002 +0100
1.3 @@ -46,20 +46,21 @@
1.4    of the type classes involved.  After finishing the proof, the theory will be
1.5    augmented by a type signature declaration corresponding to the resulting
1.6    theorem.
1.7 -
1.8 +
1.9  \item [$intro_classes$] repeatedly expands all class introduction rules of
1.10    this theory.  Note that this method usually needs not be named explicitly,
1.11 -  as it is already included in the default proof step (of $\PROOFNAME$,
1.12 -  $\BYNAME$, etc.).  In particular, instantiation of trivial (syntactic)
1.13 -  classes may be performed by a single $\DDOT$'' proof step.
1.14 +  as it is already included in the default proof step (of $\PROOFNAME$ etc.).
1.15 +  In particular, instantiation of trivial (syntactic) classes may be performed
1.16 +  by a single $\DDOT$'' proof step.
1.17
1.18  \end{descr}
1.19
1.20
1.21  \subsection{Locales and local contexts}\label{sec:locale}
1.22
1.23 -Locales are named local contexts, consisting of a declaration elements that
1.24 -are modeled after the Isar proof context (cf.\ \S\ref{sec:proof-context}).
1.25 +Locales are named local contexts, consisting of a list of declaration elements
1.26 +that are modeled after the Isar proof context commands (cf.\
1.27 +\S\ref{sec:proof-context}).
1.28
1.29  \subsubsection{Localized commands}
1.30