diff -r 5cb525437aab -r b7e6e607bb4d src/HOL/UNITY/Comp.thy --- 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 +