summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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}