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