tuned;
authorwenzelm
Thu Mar 07 19:07:56 2002 +0100 (2002-03-07)
changeset 1304002bfd6d622ca
parent 13039 cfcc1f6f21df
child 13041 6faccf7d0f25
tuned;
doc-src/IsarRef/generic.tex
     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