1.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Sun Jun 08 14:30:46 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sun Jun 08 14:31:06 2008 +0200
     1.3 @@ -392,7 +392,7 @@
     1.4      ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
     1.5      ;
     1.6  
     1.7 -    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' | 'depth\_limit' ':' nat) ')'
     1.8 +    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
     1.9      ;
    1.10      simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
    1.11        'split' (() | 'add' | 'del')) ':' thmrefs
    1.12 @@ -442,7 +442,7 @@
    1.13    ``\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharunderscore}lr{\isacharparenright}{\isachardoublequote}}'', which means that an assumption is only used
    1.14    for simplifying assumptions which are to the right of it (cf.\ \verb|asm_lr_simp_tac|).
    1.15  
    1.16 -  Giving an option ``\isa{{\isachardoublequote}{\isacharparenleft}depth{\isacharunderscore}limit{\isacharcolon}\ n{\isacharparenright}{\isachardoublequote}}'' limits the number of
    1.17 +  The configuration option \isa{{\isachardoublequote}depth{\isacharunderscore}limit{\isachardoublequote}} limits the number of
    1.18    recursive invocations of the simplifier during conditional
    1.19    rewriting.
    1.20  

     2.1 --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Sun Jun 08 14:30:46 2008 +0200
     2.2 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Sun Jun 08 14:31:06 2008 +0200
     2.3 @@ -525,7 +525,7 @@
     2.4    Note the space between \verb!@! and \verb!{! in the tabular argument.
     2.5    It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
     2.6    as an antiquotation. The styles \verb!lhs! and \verb!rhs!
     2.7 -  extract the left hand side (or right hand side respectivly) from the
     2.8 +  extract the left hand side (or right hand side respectively) from the
     2.9    conclusion of propositions consisting of a binary operator
    2.10    (e.~g.~\isa{{\isacharequal}}, \isa{{\isasymequiv}}, \isa{{\isacharless}}).
    2.11  

     3.1 --- a/doc-src/TutorialI/Protocol/document/NS_Public.tex	Sun Jun 08 14:30:46 2008 +0200
     3.2 +++ b/doc-src/TutorialI/Protocol/document/NS_Public.tex	Sun Jun 08 14:31:06 2008 +0200
     3.3 @@ -384,7 +384,7 @@
     3.4  \isaindent{{\isacharparenleft}}else\ insert\ {\isacharparenleft}Crypt\ K\ X{\isacharparenright}\ {\isacharparenleft}analz\ H{\isacharparenright}{\isacharparenright}\rulename{analz{\isacharunderscore}Crypt{\isacharunderscore}if}%
     3.5  \end{isabelle}
     3.6  The simplifier has also used \isa{Spy{\isacharunderscore}see{\isacharunderscore}priK}, proved in
     3.7 -{\S}\ref{sec:regularity}) above, to yield \isa{Ba\ {\isasymin}\ bad}.
     3.8 +{\S}\ref{sec:regularity} above, to yield \isa{Ba\ {\isasymin}\ bad}.
     3.9  
    3.10  Recall that this subgoal concerns the case
    3.11  where the last message to be sent was