summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/TutorialI/Rules/rules.tex

changeset 10578 | b32513971481 |

parent 10546 | b0ad1ed24cf6 |

child 10596 | 77951eaeb5b0 |

equal
deleted
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 |