doc-src/IsarRef/refcard.tex
changeset 8195 af2575a5c5ae
parent 7987 d9aef93c0e32
child 8203 2fcc6017cb72
     1.1 --- a/doc-src/IsarRef/refcard.tex	Fri Feb 04 21:53:36 2000 +0100
     1.2 +++ b/doc-src/IsarRef/refcard.tex	Sat Feb 05 16:54:27 2000 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4  \begin{matharray}{rcl}
     1.5    \BYY{m@1}{m@2} & \equiv & \PROOF{m@1}~\QED{m@2} \\
     1.6    \DDOT & \equiv & \BY{rule} \\
     1.7 -  \DOT & \equiv & \BY{assumption} \\
     1.8 +  \DOT & \equiv & \BY{this} \\
     1.9    \HENCENAME & \equiv & \THEN~\HAVENAME \\
    1.10    \THUSNAME & \equiv & \THEN~\SHOWNAME \\
    1.11    \FROM{a@1\;\dots\;a@n} & \equiv & \NOTE{this}{a@1\;\dots\;a@n}~\THEN \\
    1.12 @@ -79,6 +79,7 @@
    1.13  \begin{tabular}{ll}
    1.14    \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
    1.15    $assumption$ & apply some assumption \\
    1.16 +  $this$ & apply current facts \\
    1.17    $rule~a@1\;\dots\;a@n$ & apply some rule  \\
    1.18    $rule$ & apply standard rule (default for $\PROOFNAME$) \\
    1.19    $induct~x$ & apply induction rule \\