doc-src/IsarRef/generic.tex
changeset 9232 96722b04f2ae
parent 9005 67fb61748d35
child 9408 d3d56e1d2ec1
equal deleted inserted replaced
9231:8812a07d52ee 9232:96722b04f2ae
   298 \end{descr}
   298 \end{descr}
   299 
   299 
   300 
   300 
   301 \indexisaratt{standard}
   301 \indexisaratt{standard}
   302 \indexisaratt{elimify}
   302 \indexisaratt{elimify}
       
   303 \indexisaratt{no-vars}
   303 
   304 
   304 \indexisaratt{RS}\indexisaratt{COMP}
   305 \indexisaratt{RS}\indexisaratt{COMP}
   305 \indexisaratt{where}
   306 \indexisaratt{where}
   306 \indexisaratt{tag}\indexisaratt{untag}
   307 \indexisaratt{tag}\indexisaratt{untag}
   307 \indexisaratt{export}
   308 \indexisaratt{export}
   314   where & : & \isaratt \\[0.5ex]
   315   where & : & \isaratt \\[0.5ex]
   315   unfold & : & \isaratt \\
   316   unfold & : & \isaratt \\
   316   fold & : & \isaratt \\[0.5ex]
   317   fold & : & \isaratt \\[0.5ex]
   317   standard & : & \isaratt \\
   318   standard & : & \isaratt \\
   318   elimify & : & \isaratt \\
   319   elimify & : & \isaratt \\
       
   320   no_vars & : & \isaratt \\
   319   export^* & : & \isaratt \\
   321   export^* & : & \isaratt \\
   320 \end{matharray}
   322 \end{matharray}
   321 
   323 
   322 \begin{rail}
   324 \begin{rail}
   323   'tag' (nameref+)
   325   'tag' (nameref+)
   354   as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
   356   as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
   355   
   357   
   356 \item [$elimify$] turns an destruction rule into an elimination, just as the
   358 \item [$elimify$] turns an destruction rule into an elimination, just as the
   357   ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
   359   ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
   358   
   360   
       
   361 \item [$no_vars$] replaces schematic variables by free ones; this is mainly
       
   362   for tuning output of pretty printed theorems.
       
   363   
   359 \item [$export$] lifts a local result out of the current proof context,
   364 \item [$export$] lifts a local result out of the current proof context,
   360   generalizing all fixed variables and discharging all assumptions.  Note that
   365   generalizing all fixed variables and discharging all assumptions.  Note that
   361   proper incremental export is already done as part of the basic Isar
   366   proper incremental export is already done as part of the basic Isar
   362   machinery.  This attribute is mainly for experimentation.
   367   machinery.  This attribute is mainly for experimentation.
   363   
   368