# HG changeset patch
# User paulson
# Date 916740940 -3600
# Node ID b7e6e607bb4d9e61bfb4141eddd7d935c96e8bd5
# Parent  5cb525437aabf55d19befc6bb703fe7d2e269254
updated comments

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 +