diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -134,13 +134,13 @@
   apply (auto intro!: map_of_SomeI)
   done
 
-lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; ws_prog G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+"
-apply( frule r_into_trancl)
+lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; ws_prog G|] ==> D \<noteq> C \<and> \<not> (subcls1 G)^++ D C"
+apply( frule trancl.r_into_trancl [where r="subcls1 G"])
 apply( drule subcls1D)
 apply(clarify)
 apply( drule (1) class_wf_struct)
 apply( unfold ws_cdecl_def)
-apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
+apply(force simp add: reflcl_trancl' [THEN sym] simp del: reflcl_trancl')
 done
 
 lemma wf_cdecl_supD: 
@@ -149,42 +149,42 @@
 apply (auto split add: option.split_asm)
 done
 
-lemma subcls_asym: "[|ws_prog G; (C,D)\<in>(subcls1 G)^+|] ==> \<not>(D,C)\<in>(subcls1 G)^+"
-apply(erule tranclE)
+lemma subcls_asym: "[|ws_prog G; (subcls1 G)^++ C D|] ==> \<not> (subcls1 G)^++ D C"
+apply(erule trancl.cases)
 apply(fast dest!: subcls1_wfD )
-apply(fast dest!: subcls1_wfD intro: trancl_trans)
+apply(fast dest!: subcls1_wfD intro: trancl_trans')
 done
 
-lemma subcls_irrefl: "[|ws_prog G; (C,D)\<in>(subcls1 G)^+|] ==> C \<noteq> D"
-apply (erule trancl_trans_induct)
+lemma subcls_irrefl: "[|ws_prog G; (subcls1 G)^++ C D|] ==> C \<noteq> D"
+apply (erule trancl_trans_induct')
 apply  (auto dest: subcls1_wfD subcls_asym)
 done
 
-lemma acyclic_subcls1: "ws_prog G ==> acyclic (subcls1 G)"
-apply (unfold acyclic_def)
+lemma acyclic_subcls1: "ws_prog G ==> acyclicP (subcls1 G)"
+apply (simp add: acyclic_def [to_pred])
 apply (fast dest: subcls_irrefl)
 done
 
-lemma wf_subcls1: "ws_prog G ==> wf ((subcls1 G)^-1)"
-apply (rule finite_acyclic_wf)
-apply ( subst finite_converse)
+lemma wf_subcls1: "ws_prog G ==> wfP ((subcls1 G)^--1)"
+apply (rule finite_acyclic_wf [to_pred])
+apply ( subst finite_converse [to_pred])
 apply ( rule finite_subcls1)
-apply (subst acyclic_converse)
+apply (subst acyclic_converse [to_pred])
 apply (erule acyclic_subcls1)
 done
 
 
 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. (subcls1 G)^++ C D --> P D ==> P C|] ==> P C"
 (is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
 proof -
   assume p: "PROP ?P"
   assume ?A thus ?thesis apply -
 apply (drule wf_prog_ws_prog)
 apply(drule wf_subcls1)
-apply(drule wf_trancl)
-apply(simp only: trancl_converse)
-apply(erule_tac a = C in wf_induct)
+apply(drule wfP_trancl)
+apply(simp only: trancl_converse')
+apply(erule_tac a = C in wfP_induct)
 apply(rule p)
 apply(auto)
 done
@@ -225,15 +225,15 @@
 qed
 
 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. (subcls1 G)^++ C D --> P D ==> P C|] ==> P C"
 (is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
 proof -
   assume p: "PROP ?P"
   assume ?A thus ?thesis apply -
 apply(drule wf_subcls1)
-apply(drule wf_trancl)
-apply(simp only: trancl_converse)
-apply(erule_tac a = C in wf_induct)
+apply(drule wfP_trancl)
+apply(simp only: trancl_converse')
+apply(erule_tac a = C in wfP_induct)
 apply(rule p)
 apply(auto)
 done
@@ -339,7 +339,7 @@
 apply( simp (no_asm))
 apply( erule UnE)
 apply(  force)
-apply( erule r_into_rtrancl [THEN rtrancl_trans])
+apply( erule r_into_rtrancl' [THEN rtrancl_trans'])
 apply auto
 done
 
@@ -381,9 +381,9 @@
 done
 
 lemma fields_mono_lemma [rule_format (no_asm)]: 
-  "[|ws_prog G; (C',C)\<in>(subcls1 G)^*|] ==>  
+  "[|ws_prog G; (subcls1 G)^** C' C|] ==>  
   x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))"
-apply(erule converse_rtrancl_induct)
+apply(erule converse_rtrancl_induct')
 apply( safe dest!: subcls1D)
 apply(subst fields_rec)
 apply(  auto)
@@ -402,10 +402,10 @@
 "[|field (G,C) fn = Some (fd, fT); G\<turnstile>D\<preceq>C C; ws_prog G|]==>  
   map_of (fields (G,D)) (fn, fd) = Some fT"
 apply (drule field_fields)
-apply (drule rtranclD)
+apply (drule rtranclD')
 apply safe
 apply (frule subcls_is_class)
-apply (drule trancl_into_rtrancl)
+apply (drule trancl_into_rtrancl')
 apply (fast dest: fields_mono)
 done
 
@@ -437,10 +437,10 @@
 apply (frule map_of_SomeD)
 apply (clarsimp simp add: wf_cdecl_def)
 apply( clarify)
-apply( rule rtrancl_trans)
+apply( rule rtrancl_trans')
 prefer 2
 apply(  assumption)
-apply( rule r_into_rtrancl)
+apply( rule r_into_rtrancl')
 apply( fast intro: subcls1I)
 done
 
@@ -473,10 +473,10 @@
 apply (clarsimp simp add: ws_cdecl_def)
 apply blast
 apply clarify
-apply( rule rtrancl_trans)
+apply( rule rtrancl_trans')
 prefer 2
 apply(  assumption)
-apply( rule r_into_rtrancl)
+apply( rule r_into_rtrancl')
 apply( fast intro: subcls1I)
 done
 
@@ -484,15 +484,15 @@
   "[|G\<turnstile>T'\<preceq>C T; wf_prog wf_mb G|] ==>  
    \<forall>D rT b. method (G,T) sig = Some (D,rT ,b) --> 
   (\<exists>D' rT' b'. method (G,T') sig = Some (D',rT',b') \<and> G\<turnstile>D'\<preceq>C D \<and> G\<turnstile>rT'\<preceq>rT)"
-apply( drule rtranclD)
+apply( drule rtranclD')
 apply( erule disjE)
 apply(  fast)
 apply( erule conjE)
-apply( erule trancl_trans_induct)
+apply( erule trancl_trans_induct')
 prefer 2
 apply(  clarify)
 apply(  drule spec, drule spec, drule spec, erule (1) impE)
-apply(  fast elim: widen_trans rtrancl_trans)
+apply(  fast elim: widen_trans rtrancl_trans')
 apply( clarify)
 apply( drule subcls1D)
 apply( clarify)
@@ -512,7 +512,7 @@
 apply( unfold wf_cdecl_def)
 apply( drule map_of_SomeD)
 apply (auto simp add: wf_mrT_def)
-apply (rule rtrancl_trans)
+apply (rule rtrancl_trans')
 defer
 apply (rule method_wf_mhead [THEN conjunct1])
 apply (simp only: wf_prog_def)