| changeset 6138 | b7e6e607bb4d |
| parent 6012 | 1894bfc4aee9 |
| child 6295 | 351b3c2b0d83 |
--- a/src/HOL/UNITY/Comp.thy Tue Jan 19 11:15:03 1999 +0100 +++ b/src/HOL/UNITY/Comp.thy Tue Jan 19 11:15:40 1999 +0100 @@ -6,6 +6,11 @@ Composition From Chandy and Sanders, "Reasoning About Program Composition" + +QUESTIONS: + refines_def: needs the States F = States G? + + uv_prop, component: should be States F = States (F Join G) *) Comp = Union +