doc-src/IsarRef/refcard.tex
changeset 9695 ec7d7f877712
parent 9615 6eafc4d2ed85
child 9905 14a71104a498
     1.1 --- a/doc-src/IsarRef/refcard.tex	Mon Aug 28 13:50:24 2000 +0200
     1.2 +++ b/doc-src/IsarRef/refcard.tex	Mon Aug 28 13:52:38 2000 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    $\BG~\dots~\EN$ & declare explicit blocks \\
     1.5    $\NEXT$ & switch implicit blocks \\
     1.6    $\NOTE{a}{\vec b}$ & reconsider facts \\
     1.7 -  $\LET{p = t}$ & \text{abbreviate terms by higher-order matching} \\
     1.8 +  $\LET{p = t}$ & \Text{abbreviate terms by higher-order matching} \\
     1.9  \end{tabular}
    1.10  
    1.11  \begin{matharray}{rcl}
    1.12 @@ -61,13 +61,13 @@
    1.13    \MOREOVER & \approx & \NOTE{calculation}{calculation~this} \\
    1.14    \ULTIMATELY & \approx & \MOREOVER~\FROM{calculation} \\[0.5ex]
    1.15    \PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi} \\
    1.16 -%  & & \text{(permissive assumption)} \\
    1.17 +%  & & \Text{(permissive assumption)} \\
    1.18    \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\
    1.19 -%  & & \text{(definitional assumption)} \\
    1.20 +%  & & \Text{(definitional assumption)} \\
    1.21    \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi} \\
    1.22 -%  & & \text{(generalized existence)} \\
    1.23 +%  & & \Text{(generalized existence)} \\
    1.24    \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi} \\
    1.25 -%  & & \text{(named context)} \\[0.5ex]
    1.26 +%  & & \Text{(named context)} \\[0.5ex]
    1.27    \SORRY & \approx & \BY{cheating} \\
    1.28  \end{matharray}
    1.29  
    1.30 @@ -75,11 +75,11 @@
    1.31  \subsection{Diagnostic commands}
    1.32  
    1.33  \begin{matharray}{ll}
    1.34 -  \isarkeyword{pr} & \text{print current state} \\
    1.35 -  \isarkeyword{thm}~\vec a & \text{print theorems} \\
    1.36 -  \isarkeyword{term}~t & \text{print term} \\
    1.37 -  \isarkeyword{prop}~\phi & \text{print meta-level proposition} \\
    1.38 -  \isarkeyword{typ}~\tau & \text{print meta-level type} \\
    1.39 +  \isarkeyword{pr} & \Text{print current state} \\
    1.40 +  \isarkeyword{thm}~\vec a & \Text{print theorems} \\
    1.41 +  \isarkeyword{term}~t & \Text{print term} \\
    1.42 +  \isarkeyword{prop}~\phi & \Text{print meta-level proposition} \\
    1.43 +  \isarkeyword{typ}~\tau & \Text{print meta-level type} \\
    1.44  \end{matharray}
    1.45  
    1.46  
    1.47 @@ -96,11 +96,11 @@
    1.48    $induct~\vec x$ & proof by induction (provides cases) \\[2ex]
    1.49  
    1.50    \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
    1.51 -  $-$ & \text{no rules} \\
    1.52 -  $intro~\vec a$ & \text{introduction rules} \\
    1.53 -  $intro_classes$ & \text{class introduction rules} \\
    1.54 -  $elim~\vec a$ & \text{elimination rules} \\
    1.55 -  $unfold~\vec a$ & \text{definitions} \\[2ex]
    1.56 +  $-$ & \Text{no rules} \\
    1.57 +  $intro~\vec a$ & \Text{introduction rules} \\
    1.58 +  $intro_classes$ & \Text{class introduction rules} \\
    1.59 +  $elim~\vec a$ & \Text{elimination rules} \\
    1.60 +  $unfold~\vec a$ & \Text{definitions} \\[2ex]
    1.61  
    1.62    \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
    1.63    $simp$, $simp_all$ & Simplifier (+ Splitter) \\