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"uller |
3 Author: Olaf Müller |
4 Copyright 1997 TU Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
5 |
6 Some properties about (Cut ex), defined as follows: |
6 Some properties about (Cut ex), defined as follows: |
7 |
7 |
8 For every execution ex there is another shorter execution (Cut ex) |
8 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. |
9 that has the same trace as ex, but its schedule ends with an external action. |
10 |
|
11 *) |
10 *) |
12 |
11 |
13 |
12 |
14 ShortExecutions = Traces + |
13 ShortExecutions = Traces + |
15 |
14 |