doc-src/IsarRef/refcard.tex
changeset 9408 d3d56e1d2ec1
parent 9233 8c8399b9ecaa
child 9603 816917b6c2de
equal deleted inserted replaced
9407:e8f6d918fde9 9408:d3d56e1d2ec1
   125   $elimify$ & put destruction rule into elimination form \\[1ex]
   125   $elimify$ & put destruction rule into elimination form \\[1ex]
   126 
   126 
   127   \multicolumn{2}{l}{\textbf{Declare rules}} \\[0.5ex]
   127   \multicolumn{2}{l}{\textbf{Declare rules}} \\[0.5ex]
   128   $simp$ & declare Simplifier rules \\
   128   $simp$ & declare Simplifier rules \\
   129   $split$ & declare Splitter rules \\
   129   $split$ & declare Splitter rules \\
   130   $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``?'' or ``??'') \\
   130   $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``!'' or ``?'') \\
   131   $iff$ & declare Simplifier + Classical Reasoner rules \\
   131   $iff$ & declare Simplifier + Classical Reasoner rules \\
   132   $trans$ & declare calculational rules (general transitivity) \\
   132   $trans$ & declare calculational rules (general transitivity) \\
   133 \end{tabular}
   133 \end{tabular}
   134 
   134 
   135 
   135