# 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