src/HOL/TLA/Stfun.thy

--- a/src/HOL/TLA/Stfun.thy	Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Stfun.thy	Fri Jun 26 14:53:15 2015 +0200
@@ -12,7 +12,7 @@
 typedecl state
 instance state :: world ..
 
-type_synonym 'a stfun = "state => 'a"
+type_synonym 'a stfun = "state \<Rightarrow> 'a"
 type_synonym stpred  = "bool stfun"
 
 
@@ -30,14 +30,14 @@
      identifies (tuples of) "base" state variables in a specification via the
      "meta predicate" basevars, which is defined here.
   *)
-  stvars    :: "'a stfun => bool"
+  stvars    :: "'a stfun \<Rightarrow> bool"
 
 syntax
-  "_PRED"   :: "lift => 'a"                          ("PRED _")
-  "_stvars" :: "lift => bool"                        ("basevars _")
+  "_PRED"   :: "lift \<Rightarrow> 'a"                          ("PRED _")
+  "_stvars" :: "lift \<Rightarrow> bool"                        ("basevars _")
 
 translations
-  "PRED P"   =>  "(P::state => _)"
+  "PRED P"   =>  "(P::state \<Rightarrow> _)"
   "_stvars"  ==  "CONST stvars"
 
 defs
@@ -50,13 +50,13 @@
   basevars_def:  "stvars vs == range vs = UNIV"
 
 
-lemma basevars: "\<And>vs. basevars vs ==> \<exists>u. vs u = c"
+lemma basevars: "\<And>vs. basevars vs \<Longrightarrow> \<exists>u. vs u = c"
   apply (unfold basevars_def)
   apply (rule_tac b = c and f = vs in rangeE)
    apply auto
   done
 
-lemma base_pair1: "\<And>x y. basevars (x,y) ==> basevars x"
+lemma base_pair1: "\<And>x y. basevars (x,y) \<Longrightarrow> basevars x"
   apply (simp (no_asm) add: basevars_def)
   apply (rule equalityI)
    apply (rule subset_UNIV)
@@ -65,7 +65,7 @@
   apply auto
   done
 
-lemma base_pair2: "\<And>x y. basevars (x,y) ==> basevars y"
+lemma base_pair2: "\<And>x y. basevars (x,y) \<Longrightarrow> basevars y"
   apply (simp (no_asm) add: basevars_def)
   apply (rule equalityI)
    apply (rule subset_UNIV)
@@ -74,7 +74,7 @@
   apply auto
   done
 
-lemma base_pair: "\<And>x y. basevars (x,y) ==> basevars x & basevars y"
+lemma base_pair: "\<And>x y. basevars (x,y) \<Longrightarrow> basevars x & basevars y"
   apply (rule conjI)
   apply (erule base_pair1)
   apply (erule base_pair2)
@@ -89,7 +89,7 @@
   apply auto
   done
 
-lemma baseE: "[| basevars v; \<And>x. v x = c ==> Q |] ==> Q"
+lemma baseE: "\<lbrakk> basevars v; \<And>x. v x = c \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
   apply (erule basevars [THEN exE])
   apply blast
   done
@@ -99,7 +99,7 @@
    The following shows that there should not be duplicates in a "stvars" tuple:
 *)
 
-lemma "\<And>v. basevars (v::bool stfun, v) ==> False"
+lemma "\<And>v. basevars (v::bool stfun, v) \<Longrightarrow> False"
   apply (erule baseE)
   apply (subgoal_tac "(LIFT (v,v)) x = (True, False)")
    prefer 2