diff -r 4939494ed791 -r ce654b0e6d69 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -134,7 +134,7 @@
   apply (auto intro!: map_of_SomeI)
   done
 
-lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; ws_prog G|] ==> D \<noteq> C \<and> (D, C) \<notin> (subcls1 G)^+"
+lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; ws_prog G|] ==> D \<noteq> C \<and> (D, C) \<notin> (subcls1 G)\<^sup>+"
 apply( frule trancl.r_into_trancl [where r="subcls1 G"])
 apply( drule subcls1D)
 apply(clarify)
@@ -149,13 +149,13 @@
 apply (auto split: option.split_asm)
 done
 
-lemma subcls_asym: "[|ws_prog G; (C, D) \<in> (subcls1 G)^+|] ==> (D, C) \<notin> (subcls1 G)^+"
+lemma subcls_asym: "[|ws_prog G; (C, D) \<in> (subcls1 G)\<^sup>+|] ==> (D, C) \<notin> (subcls1 G)\<^sup>+"
 apply(erule trancl.cases)
 apply(fast dest!: subcls1_wfD )
 apply(fast dest!: subcls1_wfD intro: trancl_trans)
 done
 
-lemma subcls_irrefl: "[|ws_prog G; (C, D) \<in> (subcls1 G)^+|] ==> C \<noteq> D"
+lemma subcls_irrefl: "[|ws_prog G; (C, D) \<in> (subcls1 G)\<^sup>+|] ==> C \<noteq> D"
 apply (erule trancl_trans_induct)
 apply  (auto dest: subcls1_wfD subcls_asym)
 done
@@ -165,7 +165,7 @@
 apply (fast dest: subcls_irrefl)
 done
 
-lemma wf_subcls1: "ws_prog G ==> wf ((subcls1 G)^-1)"
+lemma wf_subcls1: "ws_prog G ==> wf ((subcls1 G)\<inverse>)"
 apply (rule finite_acyclic_wf)
 apply ( subst finite_converse)
 apply ( rule finite_subcls1)
@@ -174,7 +174,7 @@
 done
 
 lemma subcls_induct_struct: 
-"[|ws_prog G; !!C. \<forall>D. (C, D) \<in> (subcls1 G)^+ --> P D ==> P C|] ==> P C"
+"[|ws_prog G; !!C. \<forall>D. (C, D) \<in> (subcls1 G)\<^sup>+ --> P D ==> P C|] ==> P C"
 (is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
 proof -
   assume p: "PROP ?P"
@@ -189,7 +189,7 @@
 qed
 
 lemma subcls_induct: 
-"[|wf_prog wf_mb G; !!C. \<forall>D. (C, D) \<in> (subcls1 G)^+ --> P D ==> P C|] ==> P C"
+"[|wf_prog wf_mb G; !!C. \<forall>D. (C, D) \<in> (subcls1 G)\<^sup>+ --> P D ==> P C|] ==> P C"
 (is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
 by (fact subcls_induct_struct [OF wf_prog_ws_prog])
 
@@ -367,7 +367,7 @@
 done
 
 lemma fields_mono_lemma [rule_format (no_asm)]: 
-  "[|ws_prog G; (C', C) \<in> (subcls1 G)^*|] ==>  
+  "[|ws_prog G; (C', C) \<in> (subcls1 G)\<^sup>*|] ==>  
   x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))"
 apply(erule converse_rtrancl_induct)
 apply( safe dest!: subcls1D)