added no_vars att;
authorwenzelm
Sat Jul 01 19:58:59 2000 +0200 (2000-07-01)
changeset 923296722b04f2ae
parent 9231 8812a07d52ee
child 9233 8c8399b9ecaa
added no_vars att;
doc-src/IsarRef/generic.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Sat Jul 01 19:56:46 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Sat Jul 01 19:58:59 2000 +0200
     1.3 @@ -300,6 +300,7 @@
     1.4  
     1.5  \indexisaratt{standard}
     1.6  \indexisaratt{elimify}
     1.7 +\indexisaratt{no-vars}
     1.8  
     1.9  \indexisaratt{RS}\indexisaratt{COMP}
    1.10  \indexisaratt{where}
    1.11 @@ -316,6 +317,7 @@
    1.12    fold & : & \isaratt \\[0.5ex]
    1.13    standard & : & \isaratt \\
    1.14    elimify & : & \isaratt \\
    1.15 +  no_vars & : & \isaratt \\
    1.16    export^* & : & \isaratt \\
    1.17  \end{matharray}
    1.18  
    1.19 @@ -356,6 +358,9 @@
    1.20  \item [$elimify$] turns an destruction rule into an elimination, just as the
    1.21    ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
    1.22    
    1.23 +\item [$no_vars$] replaces schematic variables by free ones; this is mainly
    1.24 +  for tuning output of pretty printed theorems.
    1.25 +  
    1.26  \item [$export$] lifts a local result out of the current proof context,
    1.27    generalizing all fixed variables and discharging all assumptions.  Note that
    1.28    proper incremental export is already done as part of the basic Isar