
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 +




