author | paulson |
Tue, 19 Jan 1999 11:15:40 +0100 | |
changeset 6138 | b7e6e607bb4d |
parent 6137 | 5cb525437aab |
child 6139 | 26abad27b03c |
--- 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 +