src/HOL/UNITY/Simple/Mutex.thy
changeset 13812 91713a1915ee
parent 13806 fd40c9d9076b
child 16184 80617b8d33c5
     1.1 --- a/src/HOL/UNITY/Simple/Mutex.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Simple/Mutex.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -54,9 +54,10 @@
     1.4      "V4 == {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}"
     1.5  
     1.6    Mutex :: "state program"
     1.7 -    "Mutex == mk_program ({s. ~ u s & ~ v s & m s = 0 & n s = 0},
     1.8 -		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
     1.9 -			  UNIV)"
    1.10 +    "Mutex == mk_total_program
    1.11 +                 ({s. ~ u s & ~ v s & m s = 0 & n s = 0},
    1.12 +		  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
    1.13 +                  UNIV)"
    1.14  
    1.15  
    1.16    (** The correct invariants **)