doc-src/IsarRef/Thy/document/ZF_Specific.tex

   statements.  A special method assists users in this task; a version
   of this is already declared as a ``solver'' in the standard
   Simplifier setup.
 
   \begin{matharray}{rcl}
-    \indexdef{ZF}{command}{print-tcset}\mbox{\isa{\isacommand{print{\isacharunderscore}tcset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+    \indexdef{ZF}{command}{print\_tcset}\mbox{\isa{\isacommand{print{\isacharunderscore}tcset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
     \indexdef{ZF}{method}{typecheck}\mbox{\isa{typecheck}} & : & \isarmeth \\
     \indexdef{ZF}{attribute}{TC}\mbox{\isa{TC}} & : & \isaratt \\
   \end{matharray}
 
   \begin{rail}

 \begin{isamarkuptext}%
 The following important tactical tools of Isabelle/ZF have been
   ported to Isar.  These should not be used in proper proof texts.
 
   \begin{matharray}{rcl}
-    \indexdef{ZF}{method}{case-tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
-    \indexdef{ZF}{method}{induct-tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
-    \indexdef{ZF}{method}{ind-cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
-    \indexdef{ZF}{command}{inductive-cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\
+    \indexdef{ZF}{method}{case\_tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+    \indexdef{ZF}{method}{induct\_tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+    \indexdef{ZF}{method}{ind\_cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+    \indexdef{ZF}{command}{inductive\_cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\
   \end{matharray}
 
   \begin{rail}
     ('case\_tac' | 'induct\_tac') goalspec? name
     ;