changeset 3071 | 981258186b71 |
child 3275 | 3f53f2c876f4 |
3070:cadbaef4f4a5 | 3071:981258186b71 |
---|---|
1 (* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy |
|
2 ID: |
|
3 Author: Olaf M"uller |
|
4 Copyright 1997 TU Muenchen |
|
5 |
|
6 Some properties about cut(ex), defined as follows: |
|
7 |
|
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. |
|
10 |
|
11 *) |