doc-src/IsarRef/refcard.tex
changeset 13041 6faccf7d0f25
parent 13024 0461b281c2b5
child 13048 8b2eb3b78cc3
     1.1 --- a/doc-src/IsarRef/refcard.tex	Tue Mar 05 18:55:46 2002 +0100
     1.2 +++ b/doc-src/IsarRef/refcard.tex	Thu Mar 07 22:52:07 2002 +0100
     1.3 @@ -48,7 +48,7 @@
     1.4    \HENCENAME & \equiv & \THEN~\HAVENAME \\
     1.5    \THUSNAME & \equiv & \THEN~\SHOWNAME \\
     1.6    \FROM{\vec a} & \equiv & \NOTE{this}{\vec a}~\THEN \\
     1.7 -  \WITH{\vec a} & \equiv & \FROM{\vec a~this} \\[1ex]
     1.8 +  \WITH{\vec a} & \equiv & \FROM{\vec a~\AND~this} \\[1ex]
     1.9    \FROM{this} & \equiv & \THEN \\
    1.10    \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\
    1.11    \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\
    1.12 @@ -120,18 +120,18 @@
    1.13    \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
    1.14    $OF~\vec a$ & rule applied to facts (skipping ``$_$'') \\
    1.15    $of~\vec t$ & rule applied to terms (skipping ``$_$'') \\
    1.16 -  $symmetric$ & resolution with symmetry of equality \\
    1.17 -  $THEN~b$ & resolution with other rule \\
    1.18 +  $symmetric$ & resolution with symmetry rule \\
    1.19 +  $THEN~b$ & resolution with another rule \\
    1.20    $rule_format$ & result put into standard rule format \\
    1.21 -  $elim_format$ & destruct rule turned into elimination rule format \\
    1.22 -  $standard$ & result put into standard form \\[1ex]
    1.23 +  $elim_format$ & destruct rule turned into elimination rule format \\[1ex]
    1.24  
    1.25    \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]
    1.26    $simp$ & Simplifier rule \\
    1.27 -  $intro$, $elim$, $dest$ & Classical Reasoner rule \\
    1.28 +  $intro$, $elim$, $dest$ & Pure or Classical Reasoner rule \\
    1.29    $iff$ & Simplifier + Classical Reasoner rule \\
    1.30    $split$ & case split rule \\
    1.31    $trans$ & transitivity rule \\
    1.32 +  $sym$ & symmetry rule \\
    1.33  \end{tabular}
    1.34  
    1.35