doc-src/IsarRef/refcard.tex
changeset 9941 fe05af7ec816
parent 9905 14a71104a498
child 10223 31346d22bb54
     1.1 --- a/doc-src/IsarRef/refcard.tex	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/doc-src/IsarRef/refcard.tex	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -118,8 +118,8 @@
     1.4    $of~\vec t$ & rule applied to terms (skipping ``$_$'') \\
     1.5    $symmetric$ & resolution with symmetry of equality \\
     1.6    $THEN~b$ & resolution with other rule \\
     1.7 -  $rulified$ & result put into standard rule form \\
     1.8 -  $elimified$ & destruct rule turned into elimination rule \\
     1.9 +  $rule_format$ & result put into standard rule format \\
    1.10 +  $elim_format$ & destruct rule turned into elimination rule format \\
    1.11    $standard$ & result put into standard form \\[1ex]
    1.12  
    1.13    \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]