- Renamed inductive2 to inductive
- Renamed some theorems about transitive closure for predicates

--- a/src/HOL/MicroJava/BV/BVExample.thy	Wed Jul 11 11:29:44 2007 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Wed Jul 11 11:32:02 2007 +0200
@@ -67,28 +67,28 @@
 
 text {* The subclass releation spelled out: *}
 lemma subcls1:
-  "subcls1 E = member2 {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
-                (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
+  "subcls1 E = (\<lambda>C D. (C, D) \<in> {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
+                (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)})"
   apply (simp add: subcls1_def2)
   apply (simp add: name_defs class_defs system_defs E_def class_def)
-  apply (auto simp: member2_inject split: split_if_asm)
+  apply (auto simp: expand_fun_eq split: split_if_asm)
   done
 
 text {* The subclass relation is acyclic; hence its converse is well founded: *}
 lemma notin_rtrancl:
   "r\<^sup>*\<^sup>* a b \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. \<not> r a y) \<Longrightarrow> False"
-  by (auto elim: converse_rtranclE')
+  by (auto elim: converse_rtranclpE)
 
 lemma acyclic_subcls1_E: "acyclicP (subcls1 E)"
   apply (rule acyclicI [to_pred])
   apply (simp add: subcls1)
-  apply (auto dest!: tranclD')
+  apply (auto dest!: tranclpD)
   apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes)
   done
 
 lemma wf_subcls1_E: "wfP ((subcls1 E)\<inverse>\<inverse>)"
   apply (rule finite_acyclic_wf_converse [to_pred])
-  apply (simp add: subcls1)
+  apply (simp add: subcls1 del: insert_iff)
   apply (rule acyclic_subcls1_E)
   done  
 
@@ -464,7 +464,7 @@
   meta_eq_to_obj_eq [OF JType.sup_def [unfolded exec_lub_def]]
   meta_eq_to_obj_eq [OF JVM_le_unfold]
 
-lemmas [code ind] = rtrancl.rtrancl_refl converse_rtrancl_into_rtrancl'
+lemmas [code ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
 
 code_module BV
 contains

--- a/src/HOL/MicroJava/BV/JType.thy	Wed Jul 11 11:29:44 2007 +0200
+++ b/src/HOL/MicroJava/BV/JType.thy	Wed Jul 11 11:32:02 2007 +0200
@@ -78,7 +78,7 @@
     have "R \<noteq> ClassT Object \<Longrightarrow> ?thesis"
      by (auto simp add: is_ty_def is_class_def split_tupled_all
                elim!: subcls1.cases
-               elim: converse_rtranclE'
+               elim: converse_rtranclpE
                split: ref_ty.splits)
     ultimately    
     show ?thesis by blast
@@ -146,16 +146,16 @@
 apply (case_tac t)
  apply simp
 apply simp
-apply (insert rtrancl_r_diff_Id' [symmetric, standard, of "subcls1 G"])
+apply (insert rtranclp_r_diff_Id [symmetric, standard, of "subcls1 G"])
 apply simp
-apply (erule rtrancl.cases)
+apply (erule rtranclp.cases)
  apply blast
-apply (drule rtrancl_converseI')
+apply (drule rtranclp_converseI)
 apply (subgoal_tac "(inf (subcls1 G) op \<noteq>)^--1 = (inf ((subcls1 G)^--1) op \<noteq>)")
  prefer 2
  apply (simp add: converse_meet)
 apply simp
-apply (blast intro: rtrancl_into_trancl2')
+apply (blast intro: rtranclp_into_tranclp2)
 done 
 
 lemma closed_err_types:

--- a/src/HOL/MicroJava/BV/Listn.thy	Wed Jul 11 11:29:44 2007 +0200
+++ b/src/HOL/MicroJava/BV/Listn.thy	Wed Jul 11 11:32:02 2007 +0200
@@ -330,7 +330,7 @@
  apply (rename_tac m n)
  apply (case_tac "m=n")
   apply simp
- apply (fast intro!: equals0I [to_pred] dest: not_sym)
+ apply (fast intro!: equals0I [to_pred bot_empty_eq] dest: not_sym)
 apply clarify
 apply (rename_tac n)
 apply (induct_tac n)

--- a/src/HOL/MicroJava/BV/Semilat.thy	Wed Jul 11 11:29:44 2007 +0200
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Wed Jul 11 11:32:02 2007 +0200
@@ -272,22 +272,22 @@
 apply (case_tac "r^** y x")
  apply (case_tac "r^** y x'")
   apply blast
- apply (blast elim: converse_rtranclE' dest: single_valuedD)
+ apply (blast elim: converse_rtranclpE dest: single_valuedD)
 apply (rule exI)
 apply (rule conjI)
- apply (blast intro: converse_rtrancl_into_rtrancl' dest: single_valuedD)
-apply (blast intro: rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl'
-             elim: converse_rtranclE' dest: single_valuedD)
+ apply (blast intro: converse_rtranclp_into_rtranclp dest: single_valuedD)
+apply (blast intro: rtranclp.rtrancl_into_rtrancl converse_rtranclp_into_rtranclp
+             elim: converse_rtranclpE dest: single_valuedD)
 done
 
 lemma single_valued_has_lubs [rule_format]:
   "\<lbrakk> single_valuedP r; r^** x u \<rbrakk> \<Longrightarrow> (!y. r^** y u \<longrightarrow> 
   (EX z. is_lub (r^** ) x y z))"
-apply (erule converse_rtrancl_induct')
+apply (erule converse_rtranclp_induct)
  apply clarify
- apply (erule converse_rtrancl_induct')
+ apply (erule converse_rtranclp_induct)
   apply blast
- apply (blast intro: converse_rtrancl_into_rtrancl')
+ apply (blast intro: converse_rtranclp_into_rtranclp)
 apply (blast intro: extend_lub)
 done
 
@@ -313,18 +313,18 @@
 
 lemma acyclic_single_valued_finite:
  "\<lbrakk>acyclicP r; single_valuedP r; r\<^sup>*\<^sup>* x y \<rbrakk>
-  \<Longrightarrow> finite (Collect2 r \<inter> {a. r\<^sup>*\<^sup>* x a} \<times> {b. r\<^sup>*\<^sup>* b y})"
-apply(erule converse_rtrancl_induct')
+  \<Longrightarrow> finite ({(x, y). r x y} \<inter> {a. r\<^sup>*\<^sup>* x a} \<times> {b. r\<^sup>*\<^sup>* b y})"
+apply(erule converse_rtranclp_induct)
  apply(rule_tac B = "{}" in finite_subset)
   apply(simp only:acyclic_def [to_pred])
-  apply(blast intro:rtrancl_into_trancl2' rtrancl_trancl_trancl')
+  apply(blast intro:rtranclp_into_tranclp2 rtranclp_tranclp_tranclp)
  apply simp
 apply(rename_tac x x')
-apply(subgoal_tac "Collect2 r \<inter> {a. r\<^sup>*\<^sup>* x a} \<times> {b. r\<^sup>*\<^sup>* b y} =
-                   insert (x,x') (Collect2 r \<inter> {a. r\<^sup>*\<^sup>* x' a} \<times> {b. r\<^sup>*\<^sup>* b y})")
+apply(subgoal_tac "{(x, y). r x y} \<inter> {a. r\<^sup>*\<^sup>* x a} \<times> {b. r\<^sup>*\<^sup>* b y} =
+                   insert (x,x') ({(x, y). r x y} \<inter> {a. r\<^sup>*\<^sup>* x' a} \<times> {b. r\<^sup>*\<^sup>* b y})")
  apply simp
-apply(blast intro:converse_rtrancl_into_rtrancl'
-            elim:converse_rtranclE' dest:single_valuedD)
+apply(blast intro:converse_rtranclp_into_rtranclp
+            elim:converse_rtranclpE dest:single_valuedD)
 done
 
 
@@ -333,21 +333,21 @@
   exec_lub r f x y = u";
 apply(unfold exec_lub_def)
 apply(rule_tac P = "\<lambda>z. r\<^sup>*\<^sup>* y z \<and> r\<^sup>*\<^sup>* z u" and
-               r = "(Collect2 r \<inter> {(a,b). r\<^sup>*\<^sup>* y a \<and> r\<^sup>*\<^sup>* b u})^-1" in while_rule)
+               r = "({(x, y). r x y} \<inter> {(a,b). r\<^sup>*\<^sup>* y a \<and> r\<^sup>*\<^sup>* b u})^-1" in while_rule)
     apply(blast dest: is_lubD is_ubD)
    apply(erule conjE)
-   apply(erule_tac z = u in converse_rtranclE')
+   apply(erule_tac z = u in converse_rtranclpE)
     apply(blast dest: is_lubD is_ubD)
-   apply(blast dest: rtrancl.rtrancl_into_rtrancl)
+   apply(blast dest: rtranclp.rtrancl_into_rtrancl)
   apply(rename_tac s)
   apply(subgoal_tac "is_ub (r\<^sup>*\<^sup>*) x y s")
    prefer 2; apply(simp add:is_ub_def)
   apply(subgoal_tac "r\<^sup>*\<^sup>* u s")
    prefer 2; apply(blast dest:is_lubD)
-  apply(erule converse_rtranclE')
+  apply(erule converse_rtranclpE)
    apply blast
   apply(simp only:acyclic_def [to_pred])
-  apply(blast intro:rtrancl_into_trancl2' rtrancl_trancl_trancl')
+  apply(blast intro:rtranclp_into_tranclp2 rtranclp_tranclp_tranclp)
  apply(rule finite_acyclic_wf)
   apply simp
   apply(erule acyclic_single_valued_finite)
@@ -358,7 +358,7 @@
  apply blast
 apply simp
 apply(erule conjE)
-apply(erule_tac z = u in converse_rtranclE')
+apply(erule_tac z = u in converse_rtranclpE)
  apply(blast dest: is_lubD is_ubD)
 apply blast
 done

--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Wed Jul 11 11:29:44 2007 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Wed Jul 11 11:32:02 2007 +0200
@@ -404,7 +404,7 @@
        E\<turnstile>ps[::]pTs & max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')})"
 apply (simp only: wtpd_expr_def wtpd_exprs_def)
 apply (erule exE)
-apply (ind_cases2 "E \<turnstile> {C}a..mn( {pTs'}ps) :: T" for T)
+apply (ind_cases "E \<turnstile> {C}a..mn( {pTs'}ps) :: T" for T)
 apply (auto simp: max_spec_preserves_length)
 done
 
@@ -618,13 +618,13 @@
 apply simp
 apply (rule allI)
 apply (rule iffI)
-  apply (ind_cases2 "E \<turnstile> [] [::] Ts" for Ts, assumption)
+  apply (ind_cases "E \<turnstile> [] [::] Ts" for Ts, assumption)
   apply simp apply (rule WellType.Nil)
 apply (simp add: list_all2_Cons1)
 apply (rule allI)
 apply (rule iffI)
   apply (rename_tac a exs Ts)
-  apply (ind_cases2 "E \<turnstile> a # exs  [::] Ts" for a exs Ts) apply blast
+  apply (ind_cases "E \<turnstile> a # exs  [::] Ts" for a exs Ts) apply blast
   apply (auto intro: WellType.Cons)
 done
 

--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed Jul 11 11:29:44 2007 +0200
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed Jul 11 11:32:02 2007 +0200
@@ -111,7 +111,7 @@
 by (case_tac "class G C", auto simp: is_class_def dest: comp_class_imp)
 
 lemma comp_subcls1: "subcls1 (comp G) = subcls1 G"
-by (auto simp add: subcls1_def2 comp_classname comp_is_class member2_inject)
+by (auto simp add: subcls1_def2 comp_classname comp_is_class expand_fun_eq)
 
 lemma comp_widen: "widen (comp G) = widen G"
   apply (simp add: expand_fun_eq)
@@ -193,7 +193,8 @@
 apply (erule disjE)
 
   (* case class G x = None *)
-apply (simp (no_asm_simp) add: class_rec_def comp_subcls1 wfrec [to_pred] cut_apply)
+apply (simp (no_asm_simp) add: class_rec_def comp_subcls1
+  wfrec [to_pred, where r="(subcls1 G)^--1", simplified])
 apply (simp add: comp_class_None)
 
   (* case \<exists> D fs ms. (class G x = Some (D, fs, ms)) *)

--- a/src/HOL/MicroJava/J/Eval.thy	Wed Jul 11 11:29:44 2007 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Wed Jul 11 11:32:02 2007 +0200
@@ -32,7 +32,7 @@
 
   -- "Evaluation relations"
 
-inductive2
+inductive
   eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
           ("_ \<turnstile> _ -_\<succ>_-> _" [51,82,60,82,82] 81)
   and evals :: "[java_mb prog,xstate,expr list,

--- a/src/HOL/MicroJava/J/Example.thy	Wed Jul 11 11:29:44 2007 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Wed Jul 11 11:32:02 2007 +0200
@@ -173,18 +173,18 @@
 done
 
 lemma not_Object_subcls [elim!]: "(subcls1 tprg)^++ Object C ==> R"
-apply (auto dest!: tranclD' subcls1D)
+apply (auto dest!: tranclpD subcls1D)
 done
 
 lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object"
-apply (erule rtrancl_induct')
+apply (erule rtranclp_induct)
 apply  auto
 apply (drule subcls1D)
 apply auto
 done
 
 lemma not_Base_subcls_Ext [elim!]: "(subcls1 tprg)^++ Base Ext ==> R"
-apply (auto dest!: tranclD' subcls1D)
+apply (auto dest!: tranclpD subcls1D)
 done
 
 lemma class_tprgD: 
@@ -194,10 +194,10 @@
 done
 
 lemma not_class_subcls_class [elim!]: "(subcls1 tprg)^++ C C ==> R"
-apply (auto dest!: tranclD' subcls1D)
+apply (auto dest!: tranclpD subcls1D)
 apply (frule class_tprgD)
 apply (auto dest!:)
-apply (drule rtranclD')
+apply (drule rtranclpD)
 apply auto
 done
 
@@ -205,7 +205,7 @@
 apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
 done
 
-lemmas subcls_direct = subcls1I [THEN r_into_rtrancl' [where r="subcls1 G"], standard]
+lemmas subcls_direct = subcls1I [THEN r_into_rtranclp [where r="subcls1 G"], standard]
 
 lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base"
 apply (rule subcls_direct)
@@ -345,7 +345,7 @@
 apply (fold ExtC_def)
 apply (rule mp) defer apply (rule wf_foo_Ext)
 apply (auto simp add: wf_mdecl_def)
-apply (drule rtranclD')
+apply (drule rtranclpD)
 apply auto
 done
 

--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Jul 11 11:29:44 2007 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Jul 11 11:32:02 2007 +0200
@@ -27,7 +27,7 @@
 apply (case_tac "ref_ty")
 apply (clarsimp simp add: conf_def)
 apply simp
-apply (ind_cases2 "G \<turnstile> Class cname \<preceq>? Class D" for cname, simp)
+apply (ind_cases "G \<turnstile> Class cname \<preceq>? Class D" for cname, simp)
 apply (rule conf_widen, assumption+) apply (erule widen.subcls)
 
 apply (unfold cast_ok_def)
@@ -222,7 +222,7 @@
 apply( rule conjI)
 apply(  force elim!: NewC_conforms)
 apply( rule conf_obj_AddrI)
-apply(  rule_tac [2] rtrancl.rtrancl_refl)
+apply(  rule_tac [2] rtranclp.rtrancl_refl)
 apply( simp (no_asm))
 
 -- "for Cast"

--- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Jul 11 11:29:44 2007 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Jul 11 11:32:02 2007 +0200
@@ -9,7 +9,7 @@
 theory TypeRel imports Decl begin
 
 -- "direct subclass, cf. 8.1.3"
-inductive2
+inductive
   subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
   for G :: "'c prog"
 where
@@ -26,12 +26,12 @@
 done
 
 lemma subcls1_def2: 
-  "subcls1 G = member2
-     (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
+  "subcls1 G = (\<lambda>C D. (C, D) \<in>
+     (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D}))"
   by (auto simp add: is_class_def expand_fun_eq dest: subcls1D intro: subcls1I)
 
-lemma finite_subcls1: "finite (Collect2 (subcls1 G))"
-apply(simp add: subcls1_def2)
+lemma finite_subcls1: "finite {(C, D). subcls1 G C D}"
+apply(simp add: subcls1_def2 del: mem_Sigma_iff)
 apply(rule finite_SigmaI [OF finite_is_class])
 apply(rule_tac B = "{fst (the (class G C))}" in finite_subset)
 apply  auto
@@ -39,14 +39,14 @@
 
 lemma subcls_is_class: "(subcls1 G)^++ C D ==> is_class G C"
 apply (unfold is_class_def)
-apply(erule trancl_trans_induct')
+apply(erule tranclp_trans_induct)
 apply (auto dest!: subcls1D)
 done
 
 lemma subcls_is_class2 [rule_format (no_asm)]: 
   "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
 apply (unfold is_class_def)
-apply (erule rtrancl_induct')
+apply (erule rtranclp_induct)
 apply  (drule_tac [2] subcls1D)
 apply  auto
 done
@@ -54,7 +54,7 @@
 constdefs
   class_rec :: "'c prog \<Rightarrow> cname \<Rightarrow> 'a \<Rightarrow>
     (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
-  "class_rec G == wfrec (Collect2 ((subcls1 G)^--1))
+  "class_rec G == wfrec {(C, D). (subcls1 G)^--1 C D}
     (\<lambda>r C t f. case class G C of
          None \<Rightarrow> arbitrary
        | Some (D,fs,ms) \<Rightarrow> 
@@ -62,8 +62,8 @@
 
 lemma class_rec_lemma: "wfP ((subcls1 G)^--1) \<Longrightarrow> class G C = Some (D,fs,ms) \<Longrightarrow>
  class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)"
-  by (simp add: class_rec_def wfrec [to_pred]
-    cut_apply [OF Collect2I [where P="(subcls1 G)^--1"], OF conversepI, OF subcls1I])
+  by (simp add: class_rec_def wfrec [to_pred, where r="(subcls1 G)^--1", simplified]
+    cut_apply [where r="{(C, D). subcls1 G D C}", simplified, OF subcls1I])
 
 definition
   "wf_class G = wfP ((subcls1 G)^--1)"
@@ -84,8 +84,8 @@
   proof (cases "class G C")
     case None
     with wf show ?thesis
-      by (simp add: class_rec_def wfrec [to_pred]
-        cut_apply [OF Collect2I [where P="(subcls1 G)^--1"], OF conversepI, OF subcls1I])
+      by (simp add: class_rec_def wfrec [to_pred, where r="(subcls1 G)^--1", simplified]
+        cut_apply [where r="{(C, D).subcls1 G D C}", simplified, OF subcls1I])
   next
     case (Some x) show ?thesis
     proof (cases x)
@@ -142,7 +142,7 @@
 
 
 -- "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping"
-inductive2
+inductive
   widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _"   [71,71,71] 70)
   for G :: "'c prog"
 where
@@ -154,7 +154,7 @@
 
 -- "casting conversion, cf. 5.5 / 5.1.5"
 -- "left out casts on primitve types"
-inductive2
+inductive
   cast    :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
   for G :: "'c prog"
 where
@@ -168,34 +168,34 @@
 done
 
 lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> \<exists>t. T=RefT t"
-apply (ind_cases2 "G\<turnstile>RefT R\<preceq>T")
+apply (ind_cases "G\<turnstile>RefT R\<preceq>T")
 apply auto
 done
 
 lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> \<exists>t. S=RefT t"
-apply (ind_cases2 "G\<turnstile>S\<preceq>RefT R")
+apply (ind_cases "G\<turnstile>S\<preceq>RefT R")
 apply auto
 done
 
 lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> \<exists>D. T=Class D"
-apply (ind_cases2 "G\<turnstile>Class C\<preceq>T")
+apply (ind_cases "G\<turnstile>Class C\<preceq>T")
 apply auto
 done
 
 lemma widen_Class_NullT [iff]: "(G\<turnstile>Class C\<preceq>NT) = False"
 apply (rule iffI)
-apply (ind_cases2 "G\<turnstile>Class C\<preceq>NT")
+apply (ind_cases "G\<turnstile>Class C\<preceq>NT")
 apply auto
 done
 
 lemma widen_Class_Class [iff]: "(G\<turnstile>Class C\<preceq> Class D) = (G\<turnstile>C\<preceq>C D)"
 apply (rule iffI)
-apply (ind_cases2 "G\<turnstile>Class C \<preceq> Class D")
+apply (ind_cases "G\<turnstile>Class C \<preceq> Class D")
 apply (auto elim: widen.subcls)
 done
 
 lemma widen_NT_Class [simp]: "G \<turnstile> T \<preceq> NT \<Longrightarrow> G \<turnstile> T \<preceq> Class D"
-by (ind_cases2 "G \<turnstile> T \<preceq> NT",  auto)
+by (ind_cases "G \<turnstile> T \<preceq> NT",  auto)
 
 lemma cast_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>? RefT rT) = False"
 apply (rule iffI)

--- a/src/HOL/MicroJava/J/WellForm.thy	Wed Jul 11 11:29:44 2007 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Jul 11 11:32:02 2007 +0200
@@ -135,12 +135,12 @@
   done
 
 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( frule tranclp.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_tranclp [THEN sym] simp del: reflcl_tranclp)
 done
 
 lemma wf_cdecl_supD: 
@@ -150,13 +150,13 @@
 done
 
 lemma subcls_asym: "[|ws_prog G; (subcls1 G)^++ C D|] ==> \<not> (subcls1 G)^++ D C"
-apply(erule trancl.cases)
+apply(erule tranclp.cases)
 apply(fast dest!: subcls1_wfD )
-apply(fast dest!: subcls1_wfD intro: trancl_trans')
+apply(fast dest!: subcls1_wfD intro: tranclp_trans)
 done
 
 lemma subcls_irrefl: "[|ws_prog G; (subcls1 G)^++ C D|] ==> C \<noteq> D"
-apply (erule trancl_trans_induct')
+apply (erule tranclp_trans_induct)
 apply  (auto dest: subcls1_wfD subcls_asym)
 done
 
@@ -183,7 +183,7 @@
 apply (drule wf_prog_ws_prog)
 apply(drule wf_subcls1)
 apply(drule wfP_trancl)
-apply(simp only: trancl_converse')
+apply(simp only: tranclp_converse)
 apply(erule_tac a = C in wfP_induct)
 apply(rule p)
 apply(auto)
@@ -232,7 +232,7 @@
   assume ?A thus ?thesis apply -
 apply(drule wf_subcls1)
 apply(drule wfP_trancl)
-apply(simp only: trancl_converse')
+apply(simp only: tranclp_converse)
 apply(erule_tac a = C in wfP_induct)
 apply(rule p)
 apply(auto)
@@ -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_rtranclp [THEN rtranclp_trans])
 apply auto
 done
 
@@ -383,7 +383,7 @@
 lemma fields_mono_lemma [rule_format (no_asm)]: 
   "[|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_rtranclp_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 rtranclpD)
 apply safe
 apply (frule subcls_is_class)
-apply (drule trancl_into_rtrancl')
+apply (drule tranclp_into_rtranclp)
 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 rtranclp_trans)
 prefer 2
 apply(  assumption)
-apply( rule r_into_rtrancl')
+apply( rule r_into_rtranclp)
 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 rtranclp_trans)
 prefer 2
 apply(  assumption)
-apply( rule r_into_rtrancl')
+apply( rule r_into_rtranclp)
 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 rtranclpD)
 apply( erule disjE)
 apply(  fast)
 apply( erule conjE)
-apply( erule trancl_trans_induct')
+apply( erule tranclp_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 rtranclp_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 rtranclp_trans)
 defer
 apply (rule method_wf_mhead [THEN conjunct1])
 apply (simp only: wf_prog_def)

--- a/src/HOL/MicroJava/J/WellType.thy	Wed Jul 11 11:29:44 2007 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy	Wed Jul 11 11:32:02 2007 +0200
@@ -107,7 +107,7 @@
 -- "method body with parameter names, local variables, block, result expression."
 -- "local variables might include This, which is hidden anyway"
   
-inductive2
+inductive
   ty_expr :: "'c env => expr => ty => bool" ("_ \<turnstile> _ :: _" [51, 51, 51] 50)
   and ty_exprs :: "'c env => expr list => ty list => bool" ("_ \<turnstile> _ [::] _" [51, 51, 51] 50)
   and wt_stmt :: "'c env => stmt => bool" ("_ \<turnstile> _ \<surd>" [51, 51] 50)

--- a/src/HOL/Nominal/Examples/Class.thy	Wed Jul 11 11:29:44 2007 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy	Wed Jul 11 11:32:02 2007 +0200
@@ -2912,7 +2912,7 @@
   ctxtn = "(name\<times>ty) list"
   ctxtc = "(coname\<times>ty) list"
 
-inductive2
+inductive
   validc :: "ctxtc \<Rightarrow> bool"
 where
   vc1[intro]: "validc []"
@@ -2920,7 +2920,7 @@
 
 equivariance validc
 
-inductive2
+inductive
   validn :: "ctxtn \<Rightarrow> bool"
 where
   vn1[intro]: "validn []"
@@ -2944,7 +2944,7 @@
 
 declare abs_perm[eqvt]
 
-inductive2
+inductive
   fin :: "trm \<Rightarrow> name \<Rightarrow> bool"
 where
   [intro]: "fin (Ax x a) x"
@@ -3367,7 +3367,7 @@
 apply(rule fin_supp)
 done
 
-inductive2
+inductive
   fic :: "trm \<Rightarrow> coname \<Rightarrow> bool"
 where
   [intro]: "fic (Ax x a) a"
@@ -3766,7 +3766,7 @@
 apply(simp)
 done
 
-inductive2
+inductive
   l_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^isub>l _" [100,100] 100)
 where
   LAxR:  "\<lbrakk>x\<sharp>M; a\<sharp>b; fic M a\<rbrakk> \<Longrightarrow> Cut <a>.M (x).(Ax x b) \<longrightarrow>\<^isub>l M[a\<turnstile>c>b]"
@@ -4467,7 +4467,7 @@
 apply(perm_simp)+
 done
 
-inductive2
+inductive
   c_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^isub>c _" [100,100] 100)
 where
   left[intro]:  "\<lbrakk>\<not>fic M a; a\<sharp>N; x\<sharp>M\<rbrakk> \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^isub>c M{a:=(x).N}"
@@ -4532,7 +4532,7 @@
 apply(auto simp add: abs_fresh rename_fresh subst_fresh)
 done
 
-inductive2
+inductive
   a_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^isub>a _" [100,100] 100)
 where
   al_redu[intro]: "M\<longrightarrow>\<^isub>l M' \<Longrightarrow> M \<longrightarrow>\<^isub>a M'"
@@ -5269,7 +5269,7 @@
 
 lemma ax_do_not_a_star_reduce:
   shows "Ax x a \<longrightarrow>\<^isub>a* M \<Longrightarrow> M = Ax x a"
-apply(induct set: rtrancl)
+apply(induct set: rtranclp)
 apply(auto)
 apply(drule  ax_do_not_a_reduce)
 apply(simp)
@@ -5278,79 +5278,79 @@
 
 lemma a_star_CutL:
     "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^isub>a* Cut <a>.M' (x).N"
-by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma a_star_CutR:
     "N \<longrightarrow>\<^isub>a* N'\<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^isub>a* Cut <a>.M (x).N'"
-by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma a_star_Cut:
     "\<lbrakk>M \<longrightarrow>\<^isub>a* M'; N \<longrightarrow>\<^isub>a* N'\<rbrakk> \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^isub>a* Cut <a>.M' (x).N'"
-by (blast intro!: a_star_CutL a_star_CutR intro: rtrancl_trans')
+by (blast intro!: a_star_CutL a_star_CutR intro: rtranclp_trans)
 
 lemma a_star_NotR:
     "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> NotR (x).M a \<longrightarrow>\<^isub>a* NotR (x).M' a"
-by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma a_star_NotL:
     "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> NotL <a>.M x \<longrightarrow>\<^isub>a* NotL <a>.M' x"
-by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma a_star_AndRL:
     "M \<longrightarrow>\<^isub>a* M'\<Longrightarrow> AndR <a>.M <b>.N c \<longrightarrow>\<^isub>a* AndR <a>.M' <b>.N c"
-by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma a_star_AndRR:
     "N \<longrightarrow>\<^isub>a* N'\<Longrightarrow> AndR <a>.M <b>.N c \<longrightarrow>\<^isub>a* AndR <a>.M <b>.N' c"
-by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma a_star_AndR:
     "\<lbrakk>M \<longrightarrow>\<^isub>a* M'; N \<longrightarrow>\<^isub>a* N'\<rbrakk> \<Longrightarrow> AndR <a>.M <b>.N c \<longrightarrow>\<^isub>a* AndR <a>.M' <b>.N' c"
-by (blast intro!: a_star_AndRL a_star_AndRR intro: rtrancl_trans')
+by (blast intro!: a_star_AndRL a_star_AndRR intro: rtranclp_trans)
 
 lemma a_star_AndL1:
     "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> AndL1 (x).M y \<longrightarrow>\<^isub>a* AndL1 (x).M' y"
-by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma a_star_AndL2:
     "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> AndL2 (x).M y \<longrightarrow>\<^isub>a* AndL2 (x).M' y"
-by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma a_star_OrLL:
     "M \<longrightarrow>\<^isub>a* M'\<Longrightarrow> OrL (x).M (y).N z \<longrightarrow>\<^isub>a* OrL (x).M' (y).N z"
-by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma a_star_OrLR:
     "N \<longrightarrow>\<^isub>a* N'\<Longrightarrow> OrL (x).M (y).N z \<longrightarrow>\<^isub>a* OrL (x).M (y).N' z"
-by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma a_star_OrL:
     "\<lbrakk>M \<longrightarrow>\<^isub>a* M'; N \<longrightarrow>\<^isub>a* N'\<rbrakk> \<Longrightarrow> OrL (x).M (y).N z \<longrightarrow>\<^isub>a* OrL (x).M' (y).N' z"
-by (blast intro!: a_star_OrLL a_star_OrLR intro: rtrancl_trans')
+by (blast intro!: a_star_OrLL a_star_OrLR intro: rtranclp_trans)
 
 lemma a_star_OrR1:
     "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> OrR1 <a>.M b \<longrightarrow>\<^isub>a* OrR1 <a>.M' b"
-by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma a_star_OrR2:
     "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> OrR2 <a>.M b \<longrightarrow>\<^isub>a* OrR2 <a>.M' b"
-by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma a_star_ImpLL:
     "M \<longrightarrow>\<^isub>a* M'\<Longrightarrow> ImpL <a>.M (y).N z \<longrightarrow>\<^isub>a* ImpL <a>.M' (y).N z"
-by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma a_star_ImpLR:
     "N \<longrightarrow>\<^isub>a* N'\<Longrightarrow> ImpL <a>.M (y).N z \<longrightarrow>\<^isub>a* ImpL <a>.M (y).N' z"
-by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma a_star_ImpL:
     "\<lbrakk>M \<longrightarrow>\<^isub>a* M'; N \<longrightarrow>\<^isub>a* N'\<rbrakk> \<Longrightarrow> ImpL <a>.M (y).N z \<longrightarrow>\<^isub>a* ImpL <a>.M' (y).N' z"
-by (blast intro!: a_star_ImpLL a_star_ImpLR intro: rtrancl_trans')
+by (blast intro!: a_star_ImpLL a_star_ImpLR intro: rtranclp_trans)
 
 lemma a_star_ImpR:
     "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> ImpR (x).<a>.M b \<longrightarrow>\<^isub>a* ImpR (x).<a>.M' b"
-by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemmas a_star_congs = a_star_Cut a_star_NotR a_star_NotL a_star_AndR a_star_AndL1 a_star_AndL2
                       a_star_OrL a_star_OrR1 a_star_OrR2 a_star_ImpL a_star_ImpR
@@ -5359,7 +5359,7 @@
   assumes a: "NotL <a>.M x \<longrightarrow>\<^isub>a* R"
   shows "\<exists>M'. R = NotL <a>.M' x \<and> M \<longrightarrow>\<^isub>a* M'"
 using a
-apply(induct set: rtrancl)
+apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_NotL_elim)
 apply(auto)
@@ -5369,7 +5369,7 @@
   assumes a: "NotR (x).M a \<longrightarrow>\<^isub>a* R"
   shows "\<exists>M'. R = NotR (x).M' a \<and> M \<longrightarrow>\<^isub>a* M'"
 using a
-apply(induct set: rtrancl)
+apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_NotR_elim)
 apply(auto)
@@ -5379,7 +5379,7 @@
   assumes a: "AndR <a>.M <b>.N c\<longrightarrow>\<^isub>a* R"
   shows "(\<exists>M' N'. R = AndR <a>.M' <b>.N' c \<and> M \<longrightarrow>\<^isub>a* M' \<and> N \<longrightarrow>\<^isub>a* N')"
 using a
-apply(induct set: rtrancl)
+apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_AndR_elim)
 apply(auto simp add: alpha trm.inject)
@@ -5389,7 +5389,7 @@
   assumes a: "AndL1 (x).M y \<longrightarrow>\<^isub>a* R"
   shows "\<exists>M'. R = AndL1 (x).M' y \<and> M \<longrightarrow>\<^isub>a* M'"
 using a
-apply(induct set: rtrancl)
+apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_AndL1_elim)
 apply(auto simp add: alpha trm.inject)
@@ -5399,7 +5399,7 @@
   assumes a: "AndL2 (x).M y \<longrightarrow>\<^isub>a* R"
   shows "\<exists>M'. R = AndL2 (x).M' y \<and> M \<longrightarrow>\<^isub>a* M'"
 using a
-apply(induct set: rtrancl)
+apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_AndL2_elim)
 apply(auto simp add: alpha trm.inject)
@@ -5409,7 +5409,7 @@
   assumes a: "OrL (x).M (y).N z \<longrightarrow>\<^isub>a* R"
   shows "(\<exists>M' N'. R = OrL (x).M' (y).N' z \<and> M \<longrightarrow>\<^isub>a* M' \<and> N \<longrightarrow>\<^isub>a* N')"
 using a
-apply(induct set: rtrancl)
+apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_OrL_elim)
 apply(auto simp add: alpha trm.inject)
@@ -5419,7 +5419,7 @@
   assumes a: "OrR1 <a>.M y \<longrightarrow>\<^isub>a* R"
   shows "\<exists>M'. R = OrR1 <a>.M' y \<and> M \<longrightarrow>\<^isub>a* M'"
 using a
-apply(induct set: rtrancl)
+apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_OrR1_elim)
 apply(auto simp add: alpha trm.inject)
@@ -5429,7 +5429,7 @@
   assumes a: "OrR2 <a>.M y \<longrightarrow>\<^isub>a* R"
   shows "\<exists>M'. R = OrR2 <a>.M' y \<and> M \<longrightarrow>\<^isub>a* M'"
 using a
-apply(induct set: rtrancl)
+apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_OrR2_elim)
 apply(auto simp add: alpha trm.inject)
@@ -5439,7 +5439,7 @@
   assumes a: "ImpR (x).<a>.M y \<longrightarrow>\<^isub>a* R"
   shows "\<exists>M'. R = ImpR (x).<a>.M' y \<and> M \<longrightarrow>\<^isub>a* M'"
 using a
-apply(induct set: rtrancl)
+apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_ImpR_elim)
 apply(auto simp add: alpha trm.inject)
@@ -5449,7 +5449,7 @@
   assumes a: "ImpL <a>.M (y).N z \<longrightarrow>\<^isub>a* R"
   shows "(\<exists>M' N'. R = ImpL <a>.M' (y).N' z \<and> M \<longrightarrow>\<^isub>a* M' \<and> N \<longrightarrow>\<^isub>a* N')"
 using a
-apply(induct set: rtrancl)
+apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_ImpL_elim)
 apply(auto simp add: alpha trm.inject)
@@ -5788,7 +5788,7 @@
   and      b: "M \<longrightarrow>\<^isub>a* M'"
   shows "fin M' x"
 using b a
-apply(induct set: rtrancl)
+apply(induct set: rtranclp)
 apply(auto simp add: fin_a_reduce)
 done
 
@@ -5854,7 +5854,7 @@
   and      b: "M \<longrightarrow>\<^isub>a* M'"
   shows "fic M' x"
 using b a
-apply(induct set: rtrancl)
+apply(induct set: rtranclp)
 apply(auto simp add: fic_a_reduce)
 done
 
@@ -10021,7 +10021,7 @@
 
 text {* SNa *}
 
-inductive2 
+inductive 
   SNa :: "trm \<Rightarrow> bool"
 where
   SNaI: "(\<And>M'. M \<longrightarrow>\<^isub>a M' \<Longrightarrow> SNa M') \<Longrightarrow> SNa M"
@@ -19224,7 +19224,7 @@
 
 text {* typing relation *}
 
-inductive2
+inductive
    typing :: "ctxtn \<Rightarrow> trm \<Rightarrow> ctxtc \<Rightarrow> bool" ("_ \<turnstile> _ \<turnstile> _" [100,100,100] 100)
 where
   TAx:    "\<lbrakk>validn \<Gamma>;validc \<Delta>; (x,B)\<in>set \<Gamma>; (a,B)\<in>set \<Delta>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Ax x a \<turnstile> \<Delta>"