# HG changeset patch
# User paulson
# Date 995041169 -7200
# Node ID 364088045fa9f81df2df325dcf733aeb5fc65e01
# Parent  9529d31f39e02258acc9c0eaa7dc1168eaec484e
tweaks

diff -r 9529d31f39e0 -r 364088045fa9 doc-src/TutorialI/Inductive/advanced-examples.tex
--- a/doc-src/TutorialI/Inductive/advanced-examples.tex	Fri Jul 13 18:08:26 2001 +0200
+++ b/doc-src/TutorialI/Inductive/advanced-examples.tex	Fri Jul 13 18:19:29 2001 +0200
@@ -148,7 +148,7 @@
 using the function \isa{lists}. 
 \begin{isabelle}
 A\ \isasymsubseteq\ B\ \isasymLongrightarrow \ lists\ A\ \isasymsubseteq
-\ lists\ B\rulename{lists_mono}
+\ lists\ B\rulenamedx{lists_mono}
 \end{isabelle}
 %
 Why must the function be monotone?  An inductive definition describes
@@ -209,9 +209,9 @@
 \begin{isabelle}
 {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
 \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
-\ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ well\_formed\_gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well\_formed\_gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
 \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
-\ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
+\ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well\_formed\_gterm{\isacharprime}\ arity%
 \end{isabelle}
 %
 This proof resembles the one given in