# HG changeset patch
# User wenzelm
# Date 1227135833 -3600
# Node ID 87d638a4ee6762eb6c708d4a43bc9685c3572bcb
# Parent  5e009a80fe6d423cb48177bd81e6a40247d9496b
updated generated files;

diff -r 5e009a80fe6d -r 87d638a4ee67 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Nov 20 00:03:47 2008 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Nov 20 00:03:53 2008 +0100
@@ -511,6 +511,7 @@
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|=?=| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|==| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\
+    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|&&&| \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|==>| \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}} \\
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}} \\
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[|\verb,|,\verb|| \isa{prop} \verb|;| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|;| \isa{prop} \verb||\verb,|,\verb|]| \verb|==>| \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}} \\
@@ -519,18 +520,21 @@
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} \isa{idts} \verb|.| \isa{prop} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|OFCLASS| \verb|(| \isa{type} \verb|,| \isa{logic} \verb|)| \\
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|SORT_CONSTRAINT| \verb|(| \isa{type} \verb|)| \\
+    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|TERM| \isa{logic} \\
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|PROP| \isa{aprop} \\\\
 
-  \indexdef{inner}{syntax}{aprop}\hypertarget{syntax.inner.aprop}{\hyperlink{syntax.inner.aprop}{\mbox{\isa{aprop}}}} & = & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ var\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|...| \\
+  \indexdef{inner}{syntax}{aprop}\hypertarget{syntax.inner.aprop}{\hyperlink{syntax.inner.aprop}{\mbox{\isa{aprop}}}} & = & \verb|(| \isa{aprop} \verb|)| \\
+    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ var\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|...| \\
+    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|CONST| \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|CONST| \isa{{\isachardoublequote}longid{\isachardoublequote}} \\
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}logic\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ \ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ {\isasymdots}\ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}{\isachardoublequote}} \\\\
 
   \indexdef{inner}{syntax}{logic}\hypertarget{syntax.inner.logic}{\hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}}} & = & \verb|(| \isa{logic} \verb|)| \\
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}logic\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{4}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|::| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ var\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|...| \\
+    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|CONST| \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|CONST| \isa{{\isachardoublequote}longid{\isachardoublequote}} \\
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}logic\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ \ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ {\isasymdots}\ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}{\isachardoublequote}} \\
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|%| \isa{pttrns} \verb|.| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isasymlambda}} \isa{pttrns} \verb|.| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\
-    & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|CONST| \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|CONST| \isa{{\isachardoublequote}longid{\isachardoublequote}} \\
     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|TYPE| \verb|(| \isa{type} \verb|)| \\\\
 
   \indexdef{inner}{syntax}{idt}\hypertarget{syntax.inner.idt}{\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}}} & = & \verb|(| \isa{idt} \verb|)|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \\
@@ -869,7 +873,7 @@
   Priority information attached to chain productions is ignored; only
   the dummy value \isa{{\isachardoublequote}{\isacharminus}{\isadigit{1}}{\isachardoublequote}} is displayed.
 
-  \item \isa{{\isachardoublequote}print{\isacharunderscore}modes{\isachardoublequote}} lists the alternative print modes
+  \item \isa{{\isachardoublequote}print\ modes{\isachardoublequote}} lists the alternative print modes
   provided by this grammar; see \secref{sec:print-modes}.
 
   \item \isa{{\isachardoublequote}parse{\isacharunderscore}rules{\isachardoublequote}} and \isa{{\isachardoublequote}print{\isacharunderscore}rules{\isachardoublequote}} relate to
diff -r 5e009a80fe6d -r 87d638a4ee67 doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Thu Nov 20 00:03:47 2008 +0100
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Thu Nov 20 00:03:53 2008 +0100
@@ -400,7 +400,7 @@
 
   Goals may consist of multiple statements, resulting in a list of
   facts eventually.  A pending multi-goal is internally represented as
-  a meta-level conjunction (printed as \isa{{\isachardoublequote}{\isacharampersand}{\isacharampersand}{\isachardoublequote}}), which is usually
+  a meta-level conjunction (\isa{{\isachardoublequote}{\isacharampersand}{\isacharampersand}{\isacharampersand}{\isachardoublequote}}), which is usually
   split into the corresponding number of sub-goals prior to an initial
   method application, via \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}
   (\secref{sec:proof-steps}) or \indexref{}{command}{apply}\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}