equal
deleted
inserted
replaced
6 FIXME thm, theory, bind_thm(s); |
6 FIXME thm, theory, bind_thm(s); |
7 |
7 |
8 |
8 |
9 \section{Porting proof scripts} |
9 \section{Porting proof scripts} |
10 |
10 |
|
11 FIXME |
|
12 |
|
13 \subsection{Basic tactics} |
|
14 |
|
15 \begin{matharray}{llll} |
|
16 \texttt{rtac}~a~1 & & rule~a \\ |
|
17 \texttt{resolve_tac}~[a@1, \dots, a@n]~1 & & rule~a@1~\dots~a@n \\ |
|
18 \texttt{res_inst_tac}~[(x@1, t@1), \dots, (x@n, t@n)]~a~1 & & |
|
19 rule_tac~x@1 = t@1~\dots~x@n = t@n~\textrm{in}~a \\ |
|
20 |
|
21 % \texttt{} & & \\ |
|
22 \texttt{stac}~a~1 & & subst~a \\ |
|
23 \texttt{strip_tac}~1 & & intro~strip & \Text{(HOL)} \\ |
|
24 \texttt{split_all_tac} & \ll & clarify & \Text{(HOL)} \\ |
|
25 \end{matharray} |
|
26 |
|
27 |
11 \section{Performing actual proof} |
28 \section{Performing actual proof} |
12 |
29 |
13 FIXME |
30 FIXME |
14 |
31 |
15 |
32 |