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