equal
deleted
inserted
replaced
19 rule_tac~x@1 = t@1~\dots~x@n = t@n~\textrm{in}~a \\ |
19 rule_tac~x@1 = t@1~\dots~x@n = t@n~\textrm{in}~a \\ |
20 |
20 |
21 % \texttt{} & & \\ |
21 % \texttt{} & & \\ |
22 \texttt{stac}~a~1 & & subst~a \\ |
22 \texttt{stac}~a~1 & & subst~a \\ |
23 \texttt{strip_tac}~1 & & intro~strip & \Text{(HOL)} \\ |
23 \texttt{strip_tac}~1 & & intro~strip & \Text{(HOL)} \\ |
24 \texttt{split_all_tac} & \ll & clarify & \Text{(HOL)} \\ |
24 \texttt{split_all_tac} & & simp~(no_asm_simp)~only: split_paired_all & \Text{(HOL)} \\ |
|
25 & \approx & simp~only: split_tupled_all & \Text{(HOL)} \\ |
|
26 & \ll & clarify & \Text{(HOL)} \\ |
25 \end{matharray} |
27 \end{matharray} |
26 |
28 |
27 |
29 |
28 \section{Performing actual proof} |
30 \section{Performing actual proof} |
29 |
31 |