diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Memory/ProcedureInterface.thy
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Jun 26 11:07:04 2015 +0200
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Jun 26 11:44:22 2015 +0200
@@ -58,23 +58,23 @@
 defs
   slice_def:     "(PRED (x!i)) s == x s i"
 
-  caller_def:    "caller ch   == %s p. (cbit (ch s p), arg (ch s p))"
-  rtrner_def:    "rtrner ch   == %s p. (rbit (ch s p), res (ch s p))"
+  caller_def:    "caller ch   == \<lambda>s p. (cbit (ch s p), arg (ch s p))"
+  rtrner_def:    "rtrner ch   == \<lambda>s p. (rbit (ch s p), res (ch s p))"
 
-  Calling_def:   "Calling ch p  == PRED cbit< ch!p > ~= rbit< ch!p >"
-  Call_def:      "(ACT Call ch p v)   == ACT  ~ $Calling ch p
-                                     & (cbit<ch!p>$ ~= $rbit<ch!p>)
+  Calling_def:   "Calling ch p  == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
+  Call_def:      "(ACT Call ch p v)   == ACT  \<not> $Calling ch p
+                                     & (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
                                      & (arg<ch!p>$ = $v)"
   Return_def:    "(ACT Return ch p v) == ACT  $Calling ch p
                                      & (rbit<ch!p>$ = $cbit<ch!p>)
                                      & (res<ch!p>$ = $v)"
   PLegalCaller_def:      "PLegalCaller ch p == TEMP
-                             Init(~ Calling ch p)
-                             & [][ ? a. Call ch p a ]_((caller ch)!p)"
-  LegalCaller_def:       "LegalCaller ch == TEMP (! p. PLegalCaller ch p)"
+                             Init(\<not> Calling ch p)
+                             & \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
+  LegalCaller_def:       "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
   PLegalReturner_def:    "PLegalReturner ch p == TEMP
-                                [][ ? v. Return ch p v ]_((rtrner ch)!p)"
-  LegalReturner_def:     "LegalReturner ch == TEMP (! p. PLegalReturner ch p)"
+                                \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
+  LegalReturner_def:     "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)"
 
 declare slice_def [simp]