diff -r c663e675e177 -r b8ef7afe3a6b src/ZF/UNITY/Mutex.thy
--- a/src/ZF/UNITY/Mutex.thy	Sun Oct 07 15:49:25 2007 +0200
+++ b/src/ZF/UNITY/Mutex.thy	Sun Oct 07 21:19:31 2007 +0200
@@ -1,6 +1,12 @@
 (*  ID:         $Id$
     Author:     Sidi O Ehmety, Computer Laboratory
     Copyright   2001  University of Cambridge
+
+Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
+
+Variables' types are introduced globally so that type verification
+reduces to the usual ZF typechecking \<in> an ill-tyed expression will
+reduce to the empty set.
 *)
 
 header{*Mutual Exclusion*}
@@ -28,75 +34,61 @@
   u_type:  "type_of(u)=bool & default_val(u)=0"
   v_type:  "type_of(v)=bool & default_val(v)=0"
 
-constdefs
+definition
   (** The program for process U **)
-   U0 :: i
-    "U0 == {<s,t>:state*state. t = s(u:=1, m:=#1) & s`m = #0}"
+  "U0 == {<s,t>:state*state. t = s(u:=1, m:=#1) & s`m = #0}"
 
-  U1 :: i
+definition
   "U1 == {<s,t>:state*state. t = s(p:= s`v, m:=#2) &  s`m = #1}"
 
-  U2 :: i
-    "U2 == {<s,t>:state*state. t = s(m:=#3) & s`p=0 & s`m = #2}"
+definition
+  "U2 == {<s,t>:state*state. t = s(m:=#3) & s`p=0 & s`m = #2}"
 
-  U3 :: i
-    "U3 == {<s,t>:state*state. t=s(u:=0, m:=#4) & s`m = #3}"
+definition
+  "U3 == {<s,t>:state*state. t=s(u:=0, m:=#4) & s`m = #3}"
 
-  U4 :: i
-    "U4 == {<s,t>:state*state. t = s(p:=1, m:=#0) & s`m = #4}"
+definition
+  "U4 == {<s,t>:state*state. t = s(p:=1, m:=#0) & s`m = #4}"
 
 
    (** The program for process V **)
 
-  V0 :: i
-    "V0 == {<s,t>:state*state. t = s (v:=1, n:=#1) & s`n = #0}"
+definition
+  "V0 == {<s,t>:state*state. t = s (v:=1, n:=#1) & s`n = #0}"
 
-  V1 :: i
-    "V1 == {<s,t>:state*state. t = s(p:=not(s`u), n:=#2) & s`n = #1}"
+definition
+  "V1 == {<s,t>:state*state. t = s(p:=not(s`u), n:=#2) & s`n = #1}"
 
-  V2 :: i
-    "V2 == {<s,t>:state*state. t  = s(n:=#3) & s`p=1 & s`n = #2}"
+definition
+  "V2 == {<s,t>:state*state. t  = s(n:=#3) & s`p=1 & s`n = #2}"
 
-  V3 :: i
+definition
   "V3 == {<s,t>:state*state. t = s (v:=0, n:=#4) & s`n = #3}"
 
-  V4 :: i
-    "V4 == {<s,t>:state*state. t  = s (p:=0, n:=#0) & s`n = #4}"
+definition
+  "V4 == {<s,t>:state*state. t  = s (p:=0, n:=#0) & s`n = #4}"
 
- Mutex :: i
- "Mutex == mk_program({s:state. s`u=0 & s`v=0 & s`m = #0 & s`n = #0},
+definition
+  "Mutex == mk_program({s:state. s`u=0 & s`v=0 & s`m = #0 & s`n = #0},
               {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, Pow(state*state))"
 
   (** The correct invariants **)
 
-  IU :: i
-    "IU == {s:state. (s`u = 1<->(#1 $<= s`m & s`m $<= #3))
+definition
+  "IU == {s:state. (s`u = 1<->(#1 $<= s`m & s`m $<= #3))
 	             & (s`m = #3 --> s`p=0)}"
 
-  IV :: i
-    "IV == {s:state. (s`v = 1 <-> (#1 $<= s`n & s`n $<= #3))
+definition
+  "IV == {s:state. (s`v = 1 <-> (#1 $<= s`n & s`n $<= #3))
 	              & (s`n = #3 --> s`p=1)}"
 
   (** The faulty invariant (for U alone) **)
 
-  bad_IU :: i
-    "bad_IU == {s:state. (s`u = 1 <-> (#1 $<= s`m & s`m  $<= #3))&
+definition
+  "bad_IU == {s:state. (s`u = 1 <-> (#1 $<= s`m & s`m  $<= #3))&
                    (#3 $<= s`m & s`m $<= #4 --> s`p=0)}"
 
 
-(*  Title:      ZF/UNITY/Mutex.ML
-    ID:         $Id \<in> Mutex.ML,v 1.4 2003/05/27 09:39:05 paulson Exp $
-    Author:     Sidi O Ehmety, Computer Laboratory
-    Copyright   2001  University of Cambridge
-
-Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
-
-Variables' types are introduced globally so that type verification
-reduces to the usual ZF typechecking \<in> an ill-tyed expression will
-reduce to the empty set.
-
-*)
-
 (** Variables' types **)
 
 declare p_type [simp] u_type [simp] v_type [simp] m_type [simp] n_type [simp]
@@ -211,7 +203,7 @@
 (*** Progress for U ***)
 
 lemma U_F0: "Mutex \<in> {s \<in> state. s`m=#2} Unless {s \<in> state. s`m=#3}"
-by (unfold Unless_def Mutex_def, safety)
+by (unfold op_Unless_def Mutex_def, safety)
 
 lemma U_F1:
      "Mutex \<in> {s \<in> state. s`m=#1} LeadsTo {s \<in> state. s`p = s`v & s`m = #2}"
@@ -263,7 +255,7 @@
 (*** Progress for V ***)
 
 lemma V_F0: "Mutex \<in> {s \<in> state. s`n=#2} Unless {s \<in> state. s`n=#3}"
-by (unfold Unless_def Mutex_def, safety)
+by (unfold op_Unless_def Mutex_def, safety)
 
 lemma V_F1: "Mutex \<in> {s \<in> state. s`n=#1} LeadsTo {s \<in> state. s`p = not(s`u) & s`n = #2}"
 by (unfold Mutex_def, ensures_tac "V1")