src/HOL/IMP/OO.thy

   V string |
   Faccess exp string       ("_\<bullet>/_" [63,1000] 63) |
   Vassign string exp       ("(_ ::=/ _)" [1000,61] 62) |
   Fassign exp string exp   ("(_\<bullet>_ ::=/ _)" [63,0,62] 62) |
   Mcall exp string exp     ("(_\<bullet>/_<_>)" [63,0,0] 63) |
-  Semi exp exp             ("_;/ _" [61,60] 60) |
+  Seq exp exp              ("_;/ _" [61,60] 60) |
   If bexp exp exp          ("IF _/ THEN (2_)/ ELSE (2_)" [0,0,61] 61)
 and bexp = B bool | Not bexp | And bexp bexp | Eq exp exp
 
 type_synonym menv = "string \<Rightarrow> exp"
 type_synonym config = "venv \<times> store \<times> addr"

 "\<lbrakk> me \<turnstile> (oe,c\<^isub>1) \<Rightarrow> (or,c\<^isub>2);  me \<turnstile> (pe,c\<^isub>2) \<Rightarrow> (pr,ve\<^isub>3,sn\<^isub>3);
    ve = (\<lambda>x. null)(''this'' := or, ''param'' := pr);
    me \<turnstile> (me m,ve,sn\<^isub>3) \<Rightarrow> (r,ve',sn\<^isub>4) \<rbrakk>
   \<Longrightarrow>
  me \<turnstile> (oe\<bullet>m<pe>,c\<^isub>1) \<Rightarrow> (r,ve\<^isub>3,sn\<^isub>4)" |
-Semi:
+Seq:
 "\<lbrakk> me \<turnstile> (e\<^isub>1,c\<^isub>1) \<Rightarrow> (r,c\<^isub>2);  me \<turnstile> (e\<^isub>2,c\<^isub>2) \<Rightarrow> c\<^isub>3 \<rbrakk> \<Longrightarrow>
  me \<turnstile> (e\<^isub>1; e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
 IfTrue:
 "\<lbrakk> me \<turnstile> (b,c\<^isub>1) \<rightarrow> (True,c\<^isub>2);  me \<turnstile> (e\<^isub>1,c\<^isub>2) \<Rightarrow> c\<^isub>3 \<rbrakk> \<Longrightarrow>
  me \<turnstile> (IF b THEN e\<^isub>1 ELSE e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |