src/HOL/UNITY/Follows.thy
changeset 8128 3a5864b465e2
parent 8122 b43ad07660b9
child 8948 b797cfa3548d
     1.1 --- a/src/HOL/UNITY/Follows.thy	Thu Jan 13 17:36:58 2000 +0100
     1.2 +++ b/src/HOL/UNITY/Follows.thy	Fri Jan 14 12:17:53 2000 +0100
     1.3 @@ -3,13 +3,10 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1998  University of Cambridge
     1.6  
     1.7 -The Follows relation of Charpentier and Sivilotte
     1.8 -
     1.9 -The safety conditions ensures that "givenBy f" is implementable in the
    1.10 -  progress part: g cannot do anything silly.
    1.11 +The "Follows" relation of Charpentier and Sivilotte
    1.12  *)
    1.13  
    1.14 -Follows = Project +
    1.15 +Follows = SubstAx +
    1.16  
    1.17  constdefs
    1.18