author wenzelm Thu, 07 Mar 2002 19:07:56 +0100 changeset 13040 02bfd6d622ca parent 13039 cfcc1f6f21df child 13041 6faccf7d0f25
tuned;
--- a/doc-src/IsarRef/generic.tex	Thu Mar 07 19:04:00 2002 +0100
+++ b/doc-src/IsarRef/generic.tex	Thu Mar 07 19:07:56 2002 +0100
@@ -46,20 +46,21 @@
of the type classes involved.  After finishing the proof, the theory will be
augmented by a type signature declaration corresponding to the resulting
theorem.
-
+
\item [$intro_classes$] repeatedly expands all class introduction rules of
this theory.  Note that this method usually needs not be named explicitly,
-  as it is already included in the default proof step (of $\PROOFNAME$,
-  $\BYNAME$, etc.).  In particular, instantiation of trivial (syntactic)
-  classes may be performed by a single $\DDOT$'' proof step.
+  as it is already included in the default proof step (of $\PROOFNAME$ etc.).
+  In particular, instantiation of trivial (syntactic) classes may be performed
+  by a single $\DDOT$'' proof step.

\end{descr}

\subsection{Locales and local contexts}\label{sec:locale}

-Locales are named local contexts, consisting of a declaration elements that
-are modeled after the Isar proof context (cf.\ \S\ref{sec:proof-context}).
+Locales are named local contexts, consisting of a list of declaration elements
+that are modeled after the Isar proof context commands (cf.\
+\S\ref{sec:proof-context}).

\subsubsection{Localized commands}