1.1 --- a/doc-src/TutorialI/Inductive/advanced-examples.tex	Fri Jul 13 18:08:26 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Inductive/advanced-examples.tex	Fri Jul 13 18:19:29 2001 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4  using the function \isa{lists}. 
     1.5  \begin{isabelle}
     1.6  A\ \isasymsubseteq\ B\ \isasymLongrightarrow \ lists\ A\ \isasymsubseteq
     1.7 -\ lists\ B\rulename{lists_mono}
     1.8 +\ lists\ B\rulenamedx{lists_mono}
     1.9  \end{isabelle}
    1.10  %
    1.11  Why must the function be monotone?  An inductive definition describes
    1.12 @@ -209,9 +209,9 @@
    1.13  \begin{isabelle}
    1.14  {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
    1.15  \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
    1.16 -\ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
    1.17 +\ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ well\_formed\_gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well\_formed\_gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
    1.18  \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
    1.19 -\ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
    1.20 +\ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well\_formed\_gterm{\isacharprime}\ arity%
    1.21  \end{isabelle}
    1.22  %
    1.23  This proof resembles the one given in