doc-src/TutorialI/Rules/rules.tex
 changeset 10578 b32513971481 parent 10546 b0ad1ed24cf6 child 10596 77951eaeb5b0
equal inserted replaced
10577:b9c290f0343d 10578:b32513971481
1024 \bigisa{?z2} to the identity function.
1024 \bigisa{?z2} to the identity function.
1025
1025
1026 This example is typical of how Isabelle enforces sound quantifier reasoning.
1026 This example is typical of how Isabelle enforces sound quantifier reasoning.
1027
1027
1028
1028
1029 \section{Proving theorems using the \emph{\texttt{blast}} method}
1029 \section{Proving theorems using the {\tt\slshape blast} method}
1030
1030
1031 It is hard to prove substantial theorems using the methods
1031 It is hard to prove substantial theorems using the methods
1032 described above. A proof may be dozens or hundreds of steps long.  You
1032 described above. A proof may be dozens or hundreds of steps long.  You
1033 may need to search among different ways of proving certain
1033 may need to search among different ways of proving certain
1034 subgoals. Often a choice that proves one subgoal renders another
1034 subgoals. Often a choice that proves one subgoal renders another