46 \DDOT & \equiv & \BY{rule} \\ |
46 \DDOT & \equiv & \BY{rule} \\ |
47 \DOT & \equiv & \BY{this} \\ |
47 \DOT & \equiv & \BY{this} \\ |
48 \HENCENAME & \equiv & \THEN~\HAVENAME \\ |
48 \HENCENAME & \equiv & \THEN~\HAVENAME \\ |
49 \THUSNAME & \equiv & \THEN~\SHOWNAME \\ |
49 \THUSNAME & \equiv & \THEN~\SHOWNAME \\ |
50 \FROM{\vec a} & \equiv & \NOTE{this}{\vec a}~\THEN \\ |
50 \FROM{\vec a} & \equiv & \NOTE{this}{\vec a}~\THEN \\ |
51 \WITH{\vec a} & \equiv & \FROM{\vec a~this} \\[1ex] |
51 \WITH{\vec a} & \equiv & \FROM{\vec a~\AND~this} \\[1ex] |
52 \FROM{this} & \equiv & \THEN \\ |
52 \FROM{this} & \equiv & \THEN \\ |
53 \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\ |
53 \FROM{this}~\HAVENAME & \equiv & \HENCENAME \\ |
54 \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\ |
54 \FROM{this}~\SHOWNAME & \equiv & \THUSNAME \\ |
55 \end{matharray} |
55 \end{matharray} |
56 |
56 |
118 |
118 |
119 \begin{tabular}{ll} |
119 \begin{tabular}{ll} |
120 \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex] |
120 \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex] |
121 $OF~\vec a$ & rule applied to facts (skipping ``$_$'') \\ |
121 $OF~\vec a$ & rule applied to facts (skipping ``$_$'') \\ |
122 $of~\vec t$ & rule applied to terms (skipping ``$_$'') \\ |
122 $of~\vec t$ & rule applied to terms (skipping ``$_$'') \\ |
123 $symmetric$ & resolution with symmetry of equality \\ |
123 $symmetric$ & resolution with symmetry rule \\ |
124 $THEN~b$ & resolution with other rule \\ |
124 $THEN~b$ & resolution with another rule \\ |
125 $rule_format$ & result put into standard rule format \\ |
125 $rule_format$ & result put into standard rule format \\ |
126 $elim_format$ & destruct rule turned into elimination rule format \\ |
126 $elim_format$ & destruct rule turned into elimination rule format \\[1ex] |
127 $standard$ & result put into standard form \\[1ex] |
|
128 |
127 |
129 \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex] |
128 \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex] |
130 $simp$ & Simplifier rule \\ |
129 $simp$ & Simplifier rule \\ |
131 $intro$, $elim$, $dest$ & Classical Reasoner rule \\ |
130 $intro$, $elim$, $dest$ & Pure or Classical Reasoner rule \\ |
132 $iff$ & Simplifier + Classical Reasoner rule \\ |
131 $iff$ & Simplifier + Classical Reasoner rule \\ |
133 $split$ & case split rule \\ |
132 $split$ & case split rule \\ |
134 $trans$ & transitivity rule \\ |
133 $trans$ & transitivity rule \\ |
|
134 $sym$ & symmetry rule \\ |
135 \end{tabular} |
135 \end{tabular} |
136 |
136 |
137 |
137 |
138 \section{Emulating tactic scripts} |
138 \section{Emulating tactic scripts} |
139 |
139 |