--- a/src/HOL/UNITY/Alloc.thy Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Alloc.thy Tue Nov 30 16:54:10 1999 +0100
@@ -10,7 +10,7 @@
--but need invariants that values are non-negative
*)
-Alloc = Follows + Project + PPROD +
+Alloc = Follows + PPROD +
(*Duplicated from HOL/ex/NatSum.thy.
Maybe type should be [nat=>int, nat] => int**)
@@ -84,7 +84,7 @@
Increasing giv
guarantees
(INT h. {s. h <= giv s & h pfixGe ask s}
- LeadsTo
+ LeadsTo[givenBy (funPair rel ask)]
{s. tokens h <= (tokens o rel) s})"
client_spec :: clientState program set