summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Thu, 27 Aug 2015 19:55:43 +0200 | |

changeset 61028 | 99d58362eeeb |

parent 61027 | 06ceb6dcdccd |

child 61029 | b09461b3bc05 |

fixed typo in comment

--- a/src/HOL/IMP/Hoare_Examples.thy Wed Aug 26 14:59:26 2015 +0200 +++ b/src/HOL/IMP/Hoare_Examples.thy Thu Aug 27 19:55:43 2015 +0200 @@ -60,12 +60,12 @@ apply(rule Assign) apply(rule Assign') apply simp - apply(simp) + apply simp apply(rule Assign') apply simp done -text{* The proof is intentionally an apply skript because it merely composes +text{* The proof is intentionally an apply script because it merely composes the rules of Hoare logic. Of course, in a few places side conditions have to be proved. But since those proofs are 1-liners, a structured proof is overkill. In fact, we shall learn later that the application of the Hoare