src/HOL/UNITY/Alloc.thy

--- a/src/HOL/UNITY/Alloc.thy	Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/Alloc.thy	Fri Sep 10 18:40:06 1999 +0200
@@ -4,6 +4,10 @@
     Copyright   1998  University of Cambridge
 
 Specification of Chandy and Charpentier's Allocator
+
+CONSIDER CHANGING "sum" to work on type "int", not "nat"
+  --then can use subtraction in spec (1),
+  --but need invariants that values are non-negative
 *)
 
 Alloc = Follows + Extend + PPROD +