diff -r f127e949389f -r e0968e1f6fe9 src/HOL/MicroJava/JVM/JVMDefensive.thy
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy	Tue Aug 13 22:25:24 2013 +0200
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy	Tue Aug 13 22:37:58 2013 +0200
@@ -119,14 +119,11 @@
 
 definition
   exec_all_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool" 
-                   ("_ |- _ -jvmd-> _" [61,61,61]60) where
-  "G |- s -jvmd-> t \<longleftrightarrow>
+                   ("_ \<turnstile> _ \<midarrow>jvmd\<rightarrow> _" [61,61,61]60) where
+  "G \<turnstile> s \<midarrow>jvmd\<rightarrow> t \<longleftrightarrow>
          (s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union>
                   {(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"
 
-notation (xsymbols)
-  exec_all_d  ("_ \<turnstile> _ -jvmd\<rightarrow> _" [61,61,61]60)
-
 
 declare split_paired_All [simp del]
 declare split_paired_Ex [simp del]
@@ -146,9 +143,9 @@
 
 
 lemma defensive_imp_aggressive:
-  "G \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) \<Longrightarrow> G \<turnstile> s -jvm\<rightarrow> t"
+  "G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t) \<Longrightarrow> G \<turnstile> s \<midarrow>jvm\<rightarrow> t"
 proof -
-  have "\<And>x y. G \<turnstile> x -jvmd\<rightarrow> y \<Longrightarrow> \<forall>s t. x = Normal s \<longrightarrow> y = Normal t \<longrightarrow>  G \<turnstile> s -jvm\<rightarrow> t"
+  have "\<And>x y. G \<turnstile> x \<midarrow>jvmd\<rightarrow> y \<Longrightarrow> \<forall>s t. x = Normal s \<longrightarrow> y = Normal t \<longrightarrow>  G \<turnstile> s \<midarrow>jvm\<rightarrow> t"
     apply (unfold exec_all_d_def)
     apply (erule rtrancl_induct)
      apply (simp add: exec_all_def)
@@ -163,9 +160,9 @@
     apply blast
     done
   moreover
-  assume "G \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t)" 
+  assume "G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t)" 
   ultimately
-  show "G \<turnstile> s -jvm\<rightarrow> t" by blast
+  show "G \<turnstile> s \<midarrow>jvm\<rightarrow> t" by blast
 qed
 
 end
\ No newline at end of file