equal
deleted
inserted
replaced
1 (* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy |
1 (* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Olaf Müller |
3 Author: Olaf Müller |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
4 |
6 Some properties about (Cut ex), defined as follows: |
5 Some properties about (Cut ex), defined as follows: |
7 |
6 |
8 For every execution ex there is another shorter execution (Cut ex) |
7 For every execution ex there is another shorter execution (Cut ex) |
9 that has the same trace as ex, but its schedule ends with an external action. |
8 that has the same trace as ex, but its schedule ends with an external action. |