# HG changeset patch
# User wenzelm
# Date 1218569266 -7200
# Node ID 04562d200f023a16d1cca8567336862c8afbc898
# Parent  29151fa7c58e657d0513f437f4bf927df67fb1ef
updated generated file;

diff -r 29151fa7c58e -r 04562d200f02 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Aug 11 22:25:45 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Aug 12 21:27:46 2008 +0200
@@ -1064,14 +1064,14 @@
   \emph{Haskell}.
 
   \item [\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}] provides an auxiliary
-  mechanism to generate monadic code.
+  mechanism to generate monadic code for Haskell.
 
   \item [\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}] declares a list of names as
   reserved for a given target, preventing it to be shadowed by any
   generated code.
 
   \item [\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}] adds arbitrary named content
-  (``include'') to generated code.  A as last argument ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}''
+  (``include'') to generated code.  A ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument
   will remove an already added ``include''.
 
   \item [\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}] declares aliasings from
diff -r 29151fa7c58e -r 04562d200f02 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon Aug 11 22:25:45 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Tue Aug 12 21:27:46 2008 +0200
@@ -318,7 +318,7 @@
   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
   \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
   \begin{rail}
-    'locale' ('(open)')? name ('=' localeexpr)? 'begin'?
+    'locale' name ('=' localeexpr)? 'begin'?
     ;
     'print\_locale' '!'? localeexpr
     ;
@@ -429,11 +429,6 @@
   \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
   \secref{sec:object-logic}).  Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
   
-  The \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option of a locale specification prevents both
-  the current \isa{loc{\isacharunderscore}axioms} and cumulative \isa{loc} predicate
-  constructions.  Predicates are also omitted for empty specification
-  texts.
-
   \item [\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}}] prints the
   specified locale expression in a flattened form.  The notable
   special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the