src/HOL/UNITY/Follows.thy
changeset 8074 36a6c38e0eca
parent 6809 5b8912f7bb69
child 8122 b43ad07660b9
     1.1 --- a/src/HOL/UNITY/Follows.thy	Wed Dec 22 17:16:53 1999 +0100
     1.2 +++ b/src/HOL/UNITY/Follows.thy	Wed Dec 22 17:18:03 1999 +0100
     1.3 @@ -4,9 +4,12 @@
     1.4      Copyright   1998  University of Cambridge
     1.5  
     1.6  The Follows relation of Charpentier and Sivilotte
     1.7 +
     1.8 +The safety conditions ensures that "givenBy f" is implementable in the
     1.9 +  progress part: g cannot do anything silly.
    1.10  *)
    1.11  
    1.12 -Follows = Union +
    1.13 +Follows = ELT +
    1.14  
    1.15  constdefs
    1.16