src/HOL/TLA/Memory/ProcedureInterface.thy

--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Jun 26 14:53:15 2015 +0200
@@ -14,40 +14,40 @@
      rather than a single array-valued variable because the
      notation gets a little simpler.
   *)
-type_synonym ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun"
+type_synonym ('a,'r) channel =" (PrIds \<Rightarrow> ('a,'r) chan) stfun"
 
 consts
   (* data-level functions *)
-  cbit          :: "('a,'r) chan => bit"
-  rbit          :: "('a,'r) chan => bit"
-  arg           :: "('a,'r) chan => 'a"
-  res           :: "('a,'r) chan => 'r"
+  cbit          :: "('a,'r) chan \<Rightarrow> bit"
+  rbit          :: "('a,'r) chan \<Rightarrow> bit"
+  arg           :: "('a,'r) chan \<Rightarrow> 'a"
+  res           :: "('a,'r) chan \<Rightarrow> 'r"
 
   (* state functions *)
-  caller        :: "('a,'r) channel => (PrIds => (bit * 'a)) stfun"
-  rtrner        :: "('a,'r) channel => (PrIds => (bit * 'r)) stfun"
+  caller        :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'a)) stfun"
+  rtrner        :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'r)) stfun"
 
   (* state predicates *)
-  Calling   :: "('a,'r) channel => PrIds => stpred"
+  Calling   :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> stpred"
 
   (* actions *)
-  ACall      :: "('a,'r) channel => PrIds => 'a stfun => action"
-  AReturn    :: "('a,'r) channel => PrIds => 'r stfun => action"
+  ACall      :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
+  AReturn    :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
 
   (* temporal formulas *)
-  PLegalCaller      :: "('a,'r) channel => PrIds => temporal"
-  LegalCaller       :: "('a,'r) channel => temporal"
-  PLegalReturner    :: "('a,'r) channel => PrIds => temporal"
-  LegalReturner     :: "('a,'r) channel => temporal"
+  PLegalCaller      :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
+  LegalCaller       :: "('a,'r) channel \<Rightarrow> temporal"
+  PLegalReturner    :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
+  LegalReturner     :: "('a,'r) channel \<Rightarrow> temporal"
 
   (* slice through array-valued state function *)
-  slice        :: "('a => 'b) stfun => 'a => 'b stfun"
+  slice        :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
 
 syntax
-  "_slice"    :: "[lift, 'a] => lift"      ("(_!_)" [70,70] 70)
+  "_slice"    :: "[lift, 'a] \<Rightarrow> lift"      ("(_!_)" [70,70] 70)
 
-  "_Call"     :: "['a, 'b, lift] => lift"    ("(Call _ _ _)" [90,90,90] 90)
-  "_Return"   :: "['a, 'b, lift] => lift"    ("(Return _ _ _)" [90,90,90] 90)
+  "_Call"     :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Call _ _ _)" [90,90,90] 90)
+  "_Return"   :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Return _ _ _)" [90,90,90] 90)
 
 translations
   "_slice"  ==  "CONST slice"
@@ -82,10 +82,10 @@
   PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def
 
 (* Calls and returns change their subchannel *)
-lemma Call_changed: "|- Call ch p v --> <Call ch p v>_((caller ch)!p)"
+lemma Call_changed: "\<turnstile> Call ch p v \<longrightarrow> <Call ch p v>_((caller ch)!p)"
   by (auto simp: angle_def Call_def caller_def Calling_def)
 
-lemma Return_changed: "|- Return ch p v --> <Return ch p v>_((rtrner ch)!p)"
+lemma Return_changed: "\<turnstile> Return ch p v \<longrightarrow> <Return ch p v>_((rtrner ch)!p)"
   by (auto simp: angle_def Return_def rtrner_def Calling_def)
 
 end