equal
deleted
inserted
replaced
78 \isarkeyword{pr} & \text{print current state} \\ |
78 \isarkeyword{pr} & \text{print current state} \\ |
79 \isarkeyword{thm}~\vec a & \text{print theorems} \\ |
79 \isarkeyword{thm}~\vec a & \text{print theorems} \\ |
80 \isarkeyword{term}~t & \text{print term} \\ |
80 \isarkeyword{term}~t & \text{print term} \\ |
81 \isarkeyword{prop}~\phi & \text{print meta-level proposition} \\ |
81 \isarkeyword{prop}~\phi & \text{print meta-level proposition} \\ |
82 \isarkeyword{typ}~\tau & \text{print meta-level type} \\ |
82 \isarkeyword{typ}~\tau & \text{print meta-level type} \\ |
83 \isarkeyword{print_facts} & \text{print named facts} \\ |
|
84 \isarkeyword{print_binds} & \text{print term abbreviations} \\ |
|
85 \isarkeyword{print_cases} & \text{print named cases} \\ |
|
86 \end{matharray} |
83 \end{matharray} |
87 |
84 |
88 |
85 |
89 \section{Proof methods} |
86 \section{Proof methods} |
90 |
87 |
104 $intro_classes$ & \text{class introduction rules} \\ |
101 $intro_classes$ & \text{class introduction rules} \\ |
105 $elim~\vec a$ & \text{elimination rules} \\ |
102 $elim~\vec a$ & \text{elimination rules} \\ |
106 $unfold~\vec a$ & \text{definitions} \\[2ex] |
103 $unfold~\vec a$ & \text{definitions} \\[2ex] |
107 |
104 |
108 \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex] |
105 \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex] |
109 $simp$ & Simplifier (+ Splitter) \\ |
106 $simp$, $simp_all$ & Simplifier (+ Splitter) \\ |
110 $blast$, $fast$ & Classical Reasoner \\ |
107 $blast$, $fast$ & Classical Reasoner \\ |
111 $force$, $auto$ & Simplifier + Classical Reasoner \\ |
108 $auto$, $force$ & Simplifier + Classical Reasoner \\ |
112 $arith$ & Arithmetic procedure \\ |
109 $arith$ & Arithmetic procedure \\ |
113 \end{tabular} |
110 \end{tabular} |
114 |
111 |
115 |
112 |
116 \section{Attributes} |
113 \section{Attributes} |
146 \end{tabular} |
143 \end{tabular} |
147 |
144 |
148 \subsection{Methods} |
145 \subsection{Methods} |
149 |
146 |
150 \begin{tabular}{ll} |
147 \begin{tabular}{ll} |
151 $tactic~text$ & method from ML tactic \\ |
148 $rule_tac~insts$ & resolution with instantiation \\ |
152 $insert~\vec a$ & insert theorems (ignoring current facts) \\ |
149 $erule_tac~insts$ & elim-resolution with instantiation \\ |
153 $res_inst_tac~insts$ & resolution with instantiation \\ |
150 $drule_tac~insts$ & destruct-resolution with instantiation \\ |
154 $eres_inst_tac~insts$ & elim-resolution with instantiation \\ |
151 $frule_tac~insts$ & forward-resolution with instantiation \\ |
155 $dres_inst_tac~insts$ & destruct-resolution with instantiation \\ |
152 $subgoal_tac~\phi$ & insert new claims \\ |
156 $forw_inst_tac~insts$ & forward-resolution with instantiation \\ |
|
157 $subgoal_tac~\phi$ & insert new claim \\ |
|
158 $case_tac~t$ & exhaustion (datatypes) \\ |
153 $case_tac~t$ & exhaustion (datatypes) \\ |
159 $induct_tac~\vec x$ & induction (datatypes) \\ |
154 $induct_tac~\vec x$ & induction (datatypes) \\ |
|
155 $tactic~text$ & method from ML tactic \\ |
160 \end{tabular} |
156 \end{tabular} |
161 |
157 |
162 |
158 |
163 %%% Local Variables: |
159 %%% Local Variables: |
164 %%% mode: latex |
160 %%% mode: latex |