doc-src/IsarRef/generic.tex
changeset 9941 fe05af7ec816
parent 9936 f080397656d8
child 10031 12fd0fcf755a
     1.1 --- a/doc-src/IsarRef/generic.tex	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -305,7 +305,7 @@
     1.4  
     1.5  
     1.6  \indexisaratt{standard}
     1.7 -\indexisaratt{elimified}
     1.8 +\indexisaratt{elim-format}
     1.9  \indexisaratt{no-vars}
    1.10  
    1.11  \indexisaratt{THEN}\indexisaratt{COMP}
    1.12 @@ -320,7 +320,7 @@
    1.13    unfolded & : & \isaratt \\
    1.14    folded & : & \isaratt \\[0.5ex]
    1.15    standard & : & \isaratt \\
    1.16 -  elimified & : & \isaratt \\
    1.17 +  elim_format & : & \isaratt \\
    1.18    no_vars^* & : & \isaratt \\
    1.19    exported^* & : & \isaratt \\
    1.20  \end{matharray}
    1.21 @@ -356,8 +356,8 @@
    1.22    given meta-level definitions throughout a rule.
    1.23  \item [$standard$] puts a theorem into the standard form of object-rules, just
    1.24    as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
    1.25 -\item [$elimified$] turns an destruction rule into an elimination, just as the
    1.26 -  ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
    1.27 +\item [$elim_format$] turns a destruction rule into elimination rule format;
    1.28 +  see also the ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
    1.29  \item [$no_vars$] replaces schematic variables by free ones; this is mainly
    1.30    for tuning output of pretty printed theorems.
    1.31  \item [$exported$] lifts a local result out of the current proof context,