src/HOL/UNITY/Comp.thy
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 +