changeset 41959 | b460124855b8 |
parent 37591 | d3daea901123 |
child 42054 | 8cd4783904d8 |
41958:5abc60a017e0 | 41959:b460124855b8 |
---|---|
1 (* Title: HOL/Hoare/HoareAbort.thy |
1 (* Title: HOL/Hoare/Hoare_Logic_Abort.thy |
2 Author: Leonor Prensa Nieto & Tobias Nipkow |
2 Author: Leonor Prensa Nieto & Tobias Nipkow |
3 Copyright 2003 TUM |
3 Copyright 2003 TUM |
4 |
4 |
5 Like Hoare.thy, but with an Abort statement for modelling run time errors. |
5 Like Hoare.thy, but with an Abort statement for modelling run time errors. |
6 *) |
6 *) |