# HG changeset patch # User ballarin # Date 1157376420 -7200 # Node ID 0bda06d731ee73d4b805e2762e5143c5590d43ea # Parent 210b326a03c95c75a285b91a581075e4bc565bda Documented methods intro_locales and unfold_locales. diff -r 210b326a03c9 -r 0bda06d731ee doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Mon Sep 04 13:55:32 2006 +0200 +++ b/doc-src/IsarRef/generic.tex Mon Sep 04 15:27:00 2006 +0200 @@ -204,6 +204,8 @@ \isarcmd{locale} & : & \isartrans{theory}{local{\dsh}theory} \\ \isarcmd{print_locale}^* & : & \isarkeep{theory~|~proof} \\ \isarcmd{print_locales}^* & : & \isarkeep{theory~|~proof} \\ + intro_locales & : & \isarmeth \\ + unfold_locales & : & \isarmeth \\ \end{matharray} \indexouternonterm{contextexpr}\indexouternonterm{contextelem} @@ -330,6 +332,16 @@ \item [$\isarkeyword{print_locales}$] prints the names of all locales of the current theory. +\item [$intro_locales$ and $unfold_locales$] repeatedly expand + all introduction rules of locale predicates of the theory. While + $intro_locales$ only applies the $loc.intro$ introduction rules and + therefore does not decend to assumptions, $unfold_locales$ is more + aggressive and applies $loc_axioms.intro$ as well. Both methods are + aware of locale specifications entailed by the context, both from + target and $\isarkeyword{includes}$ statements, and from + interpretations (see below). New goals that are entailed by the + current context are discharged automatically. + \end{descr} @@ -470,7 +482,7 @@ \end{warn} -\subsubsection{Constructive type classes} +\subsection{Constructive type classes} A special case of locales are constructive type classes. Constructive type classes