# HG changeset patch
# User wenzelm
# Date 1212928266 -7200
# Node ID 2cf13a72e1704d0094d21e7dc68e7271a282ed31
# Parent  66d6da816be70ff6fca3d800a031a64bd481224b
updated generated file;

diff -r 66d6da816be7 -r 2cf13a72e170 doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Sun Jun 08 14:30:46 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sun Jun 08 14:31:06 2008 +0200
@@ -392,7 +392,7 @@
     ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
     ;
 
-    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' | 'depth\_limit' ':' nat) ')'
+    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
     ;
     simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
       'split' (() | 'add' | 'del')) ':' thmrefs
@@ -442,7 +442,7 @@
   ``\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharunderscore}lr{\isacharparenright}{\isachardoublequote}}'', which means that an assumption is only used
   for simplifying assumptions which are to the right of it (cf.\ \verb|asm_lr_simp_tac|).
 
-  Giving an option ``\isa{{\isachardoublequote}{\isacharparenleft}depth{\isacharunderscore}limit{\isacharcolon}\ n{\isacharparenright}{\isachardoublequote}}'' limits the number of
+  The configuration option \isa{{\isachardoublequote}depth{\isacharunderscore}limit{\isachardoublequote}} limits the number of
   recursive invocations of the simplifier during conditional
   rewriting.
 
diff -r 66d6da816be7 -r 2cf13a72e170 doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Sun Jun 08 14:30:46 2008 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Sun Jun 08 14:31:06 2008 +0200
@@ -525,7 +525,7 @@
   Note the space between \verb!@! and \verb!{! in the tabular argument.
   It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
   as an antiquotation. The styles \verb!lhs! and \verb!rhs!
-  extract the left hand side (or right hand side respectivly) from the
+  extract the left hand side (or right hand side respectively) from the
   conclusion of propositions consisting of a binary operator
   (e.~g.~\isa{{\isacharequal}}, \isa{{\isasymequiv}}, \isa{{\isacharless}}).
 
diff -r 66d6da816be7 -r 2cf13a72e170 doc-src/TutorialI/Protocol/document/NS_Public.tex
--- a/doc-src/TutorialI/Protocol/document/NS_Public.tex	Sun Jun 08 14:30:46 2008 +0200
+++ b/doc-src/TutorialI/Protocol/document/NS_Public.tex	Sun Jun 08 14:31:06 2008 +0200
@@ -384,7 +384,7 @@
 \isaindent{{\isacharparenleft}}else\ insert\ {\isacharparenleft}Crypt\ K\ X{\isacharparenright}\ {\isacharparenleft}analz\ H{\isacharparenright}{\isacharparenright}\rulename{analz{\isacharunderscore}Crypt{\isacharunderscore}if}%
 \end{isabelle}
 The simplifier has also used \isa{Spy{\isacharunderscore}see{\isacharunderscore}priK}, proved in
-{\S}\ref{sec:regularity}) above, to yield \isa{Ba\ {\isasymin}\ bad}.
+{\S}\ref{sec:regularity} above, to yield \isa{Ba\ {\isasymin}\ bad}.
 
 Recall that this subgoal concerns the case
 where the last message to be sent was