111 |
111 |
112 |
112 |
113 \section{Attributes} |
113 \section{Attributes} |
114 |
114 |
115 \begin{tabular}{ll} |
115 \begin{tabular}{ll} |
116 \multicolumn{2}{l}{\textbf{Manipulate rules}} \\[0.5ex] |
116 \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex] |
117 $OF~\vec a$ & apply rule to facts (skipping ``$_$'') \\ |
117 $OF~\vec a$ & rule applied to facts (skipping ``$_$'') \\ |
118 $of~\vec t$ & apply rule to terms (skipping ``$_$'') \\ |
118 $of~\vec t$ & rule applied to terms (skipping ``$_$'') \\ |
119 $THEN~b$ & resolve fact with rule \\ |
119 $symmetric$ & resolution with symmetry of equality \\ |
120 $symmetric$ & apply symmetry of equality \\ |
120 $THEN~b$ & resolution with other rule \\ |
121 $standard$ & put into standard result form \\ |
121 $rulified$ & result put into standard rule form \\ |
122 $rulify$ & put into object-rule form \\ |
122 $elimified$ & destruct rule turned into elimination rule \\ |
123 $elimify$ & put destruction rule into elimination form \\[1ex] |
123 $standard$ & result put into standard form \\[1ex] |
124 |
124 |
125 \multicolumn{2}{l}{\textbf{Declare rules}} \\[0.5ex] |
125 \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex] |
126 $simp$ & declare Simplifier rules \\ |
126 $simp$ & Simplifier rule \\ |
127 $split$ & declare Splitter rules \\ |
127 $intro$, $elim$, $dest$ & Classical Reasoner rule \\ |
128 $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``!'' or ``?'') \\ |
128 $iff$ & Simplifier + Classical Reasoner rule \\ |
129 $iff$ & declare Simplifier + Classical Reasoner rules \\ |
129 $split$ & case split rule \\ |
130 $trans$ & declare calculational rules (general transitivity) \\ |
130 $trans$ & transitivity rule \\ |
131 \end{tabular} |
131 \end{tabular} |
132 |
132 |
133 |
133 |
134 \section{Emulating tactic scripts} |
134 \section{Emulating tactic scripts} |
135 |
135 |