equal
deleted
inserted
replaced
5 the theorems represent states of a backward proof. Tactics seldom |
5 the theorems represent states of a backward proof. Tactics seldom |
6 need to be coded from scratch, as functions; instead they are |
6 need to be coded from scratch, as functions; instead they are |
7 expressed using basic tactics and tacticals. |
7 expressed using basic tactics and tacticals. |
8 |
8 |
9 This chapter only presents the primitive tactics. Substantial proofs require |
9 This chapter only presents the primitive tactics. Substantial proofs require |
10 the power of simplification (Chapter~\ref{simp-chap}) and classical reasoning |
10 the power of simplification (Chapter~\ref{chap:simplification}) and classical |
11 (Chapter~\ref{chap:classical}). |
11 reasoning (Chapter~\ref{chap:classical}). |
12 |
12 |
13 \section{Resolution and assumption tactics} |
13 \section{Resolution and assumption tactics} |
14 {\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using |
14 {\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using |
15 a rule. {\bf Elim-resolution} is particularly suited for elimination |
15 a rule. {\bf Elim-resolution} is particularly suited for elimination |
16 rules, while {\bf destruct-resolution} is particularly suited for |
16 rules, while {\bf destruct-resolution} is particularly suited for |