1.1 --- a/doc-src/IsarRef/refcard.tex Sat Oct 30 20:41:30 1999 +0200
1.2 +++ b/doc-src/IsarRef/refcard.tex Sun Oct 31 15:20:35 1999 +0100
1.3 @@ -14,13 +14,13 @@
1.4 $\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\
1.5 $\BG~\dots~\EN$ & declare explicit blocks \\
1.6 $\isarcmd{next}$ & switch implicit blocks \\
1.7 - $\NOTE{a}{a@1~\dots~a@n}$ & reconsider facts \\
1.8 - $\LET{p = t}$ & \text{abbreviate terms by matching} \\
1.9 + $\NOTE{a}{a@1\;\dots\;a@n}$ & reconsider facts \\
1.10 + $\LET{p = t}$ & \text{abbreviate terms by higher-order matching} \\
1.11 \end{tabular}
1.12
1.13 \begin{matharray}{rcl}
1.14 - theory{\dsh}stmt & = & \THEOREM{name}{form} ~proof \\
1.15 - & \Or & \LEMMA{name}{form}~proof \\
1.16 + theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\
1.17 + & \Or & \LEMMA{name}{prop}~proof \\
1.18 & \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex]
1.19 proof & = & \PROOF{method}~stmt^*~\QED{method} \\[1ex]
1.20 stmt & = & \BG~stmt^*~\EN \\
1.21 @@ -28,11 +28,11 @@
1.22 & \Or & \NOTE{name}{name^+} \\
1.23 & \Or & \LET{term = term} \\[0.5ex]
1.24 & \Or & \FIX{var^+} \\
1.25 - & \Or & \ASSUME{name}{form^+}\\
1.26 + & \Or & \ASSUME{name}{prop^+}\\
1.27 & \Or & \THEN~goal{\dsh}stmt \\
1.28 & \Or & goal{\dsh}stmt \\
1.29 - goal{\dsh}stmt & = & \HAVE{name}{form}~proof \\
1.30 - & \Or & \SHOW{name}{form}~proof \\
1.31 + goal{\dsh}stmt & = & \HAVE{name}{prop}~proof \\
1.32 + & \Or & \SHOW{name}{prop}~proof \\
1.33 \end{matharray}
1.34
1.35
1.36 @@ -44,8 +44,8 @@
1.37 \DOT & \equiv & \BY{assumption} \\
1.38 \HENCENAME & \equiv & \THEN~\HAVENAME \\
1.39 \THUSNAME & \equiv & \THEN~\SHOWNAME \\
1.40 - \FROM{a@1~\dots~a@n} & \equiv & \NOTE{this}{a@1~\dots~a@n}~\THEN \\
1.41 - \WITH{a@1~\dots~a@n} & \equiv & \FROM{a@1~\dots~a@n~this} \\[1ex]
1.42 + \FROM{a@1\;\dots\;a@n} & \equiv & \NOTE{this}{a@1\;\dots\;a@n}~\THEN \\
1.43 + \WITH{a@1\;\dots\;a@n} & \equiv & \FROM{a@1\;\dots\;a@n~this} \\[1ex]
1.44 \FROM{this} & \equiv & \THEN \\
1.45 \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\
1.46 \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\
1.47 @@ -67,7 +67,7 @@
1.48 \subsection{Diagnostic commands}
1.49
1.50 \begin{matharray}{ll}
1.51 - \isarcmd{thm}~a@1~\dots~a@n & \text{print theorems} \\
1.52 + \isarcmd{thm}~a@1\;\dots\;a@n & \text{print theorems} \\
1.53 \isarcmd{term}~t & \text{print term} \\
1.54 \isarcmd{prop}~\phi & \text{print meta-level proposition} \\
1.55 \isarcmd{typ}~\tau & \text{print meta-level type} \\
1.56 @@ -78,22 +78,22 @@
1.57
1.58 \begin{tabular}{ll}
1.59 \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
1.60 - $assumption$ & apply assumption \\
1.61 - $rule~a@1~\dots~a@n$ & apply some rule \\
1.62 + $assumption$ & apply some assumption \\
1.63 + $rule~a@1\;\dots\;a@n$ & apply some rule \\
1.64 $rule$ & apply standard rule (default for $\PROOFNAME$) \\
1.65 $induct~x$ & apply induction rule \\
1.66 - $contradiction$ & apply $\neg{}$ elimination rule \\[2ex]
1.67 + $contradiction$ & apply $\neg{}$ elimination rule (any order) \\[2ex]
1.68
1.69 \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
1.70 $-$ & \text{no rules} \\
1.71 - $intro~a@1~\dots~a@n$ & \text{introduction rules} \\
1.72 - $elim~a@1~\dots~a@n$ & \text{elimination rules} \\
1.73 - $unfold~a@1~\dots~a@n$ & \text{definitions} \\[2ex]
1.74 + $intro~a@1\;\dots\;a@n$ & \text{introduction rules} \\
1.75 + $elim~a@1\;\dots\;a@n$ & \text{elimination rules} \\
1.76 + $unfold~a@1\;\dots\;a@n$ & \text{definitions} \\[2ex]
1.77
1.78 \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
1.79 $simp$ & Simplifier \\
1.80 - $blast$, $fast$ & Classical reasoner \\
1.81 - $force$, $auto$ & Simplifier + Classical reasoner \\
1.82 + $blast$, $fast$ & Classical Reasoner \\
1.83 + $force$, $auto$ & Simplifier + Classical Reasoner \\
1.84 $arith$ & Arithmetic procedure \\
1.85 \end{tabular}
1.86
1.87 @@ -102,8 +102,8 @@
1.88
1.89 \begin{tabular}{ll}
1.90 \multicolumn{2}{l}{\textbf{Modify rules}} \\[0.5ex]
1.91 - $OF~a@1~\dots~a@n$ & apply rule to facts (skip ``$_$'') \\
1.92 - $of~t@1~\dots~t@n$ & apply rule to terms (skip ``$_$'') \\
1.93 + $OF~a@1\;\dots\;a@n$ & apply rule to facts (skipping ``$_$'') \\
1.94 + $of~t@1\;\dots\;t@n$ & apply rule to terms (skipping ``$_$'') \\
1.95 $RS~b$ & resolve fact with rule \\
1.96 $standard$ & put into standard result form \\
1.97 $rulify$ & put into object-rule form \\
1.98 @@ -111,12 +111,11 @@
1.99
1.100 \multicolumn{2}{l}{\textbf{Modify context}} \\[0.5ex]
1.101 $simp$ & declare Simplifier rules \\
1.102 - $intro$, $elim$, $dest$ & declare Classical reasoner rules (also ``$!$'' or ``$!!$'') \\
1.103 - $iff$ & declare Simplifier + Classical reasoner rules \\
1.104 - $trans$ & calculational rules (general transitivity) \\
1.105 + $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``$!$'' or ``$!!$'') \\
1.106 + $iff$ & declare Simplifier + Classical Reasoner rules \\
1.107 + $trans$ & declare calculational rules (general transitivity) \\
1.108 \end{tabular}
1.109
1.110 -
1.111 %%% Local Variables:
1.112 %%% mode: latex
1.113 %%% TeX-master: "isar-ref"