# HG changeset patch
# User berghofe
# Date 1184145394 -7200
# Node ID b07cff284683589712db4857f8e82bd3b445b0cd
# Parent  a455e69c31cc8a44cd983a03e6ae623239f2acfc
Renamed inductive2 to inductive.

diff -r a455e69c31cc -r b07cff284683 src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/AxSem.thy	Wed Jul 11 11:16:34 2007 +0200
@@ -476,7 +476,7 @@
 change_claset (fn cs => cs delSWrapper "split_all_tac");
 *}
 
-inductive2
+inductive
   ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57)
   and ax_deriv :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triple  \<Rightarrow> bool" ("_,_\<turnstile>_" [61,58,58] 57)
   for G :: prog
diff -r a455e69c31cc -r b07cff284683 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy	Wed Jul 11 11:16:34 2007 +0200
@@ -541,7 +541,7 @@
    below
 *)
 
-inductive2
+inductive
   members :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
     ("_ \<turnstile> _ member'_of _" [61,61,61] 60)
   for G :: prog
@@ -634,7 +634,7 @@
 
 text {* Static overriding (used during the typecheck of the compiler) *}
 
-inductive2
+inductive
   stat_overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
     ("_ \<turnstile> _ overrides\<^sub>S _" [61,61,61] 60)
   for G :: prog
@@ -653,7 +653,7 @@
 
 text {* Dynamic overriding (used during the typecheck of the compiler) *}
 
-inductive2
+inductive
   overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
     ("_ \<turnstile> _ overrides _" [61,61,61] 60)
   for G :: prog
@@ -784,7 +784,7 @@
 \end{itemize} 
 *} 
 
-inductive2
+inductive
   accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   and accessible_from :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
     ("_ \<turnstile> _ of _ accessible'_from _" [61,61,61,61] 60)
@@ -828,7 +828,7 @@
 "G\<turnstile>Field fn f of C accessible_from accclass"  
  \<rightleftharpoons> "G\<turnstile>(fieldm fn f) of C accessible_from accclass" 
 
-inductive2
+inductive
   dyn_accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   and dyn_accessible_from' ::  "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
     ("_ \<turnstile> _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
diff -r a455e69c31cc -r b07cff284683 src/HOL/Bali/DefiniteAssignment.thy
--- a/src/HOL/Bali/DefiniteAssignment.thy	Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy	Wed Jul 11 11:16:34 2007 +0200
@@ -533,7 +533,7 @@
 distinguish boolean and other expressions.
 *}
 
-inductive2
+inductive
   da :: "env \<Rightarrow> lname set \<Rightarrow> term \<Rightarrow> assigned \<Rightarrow> bool" ("_\<turnstile> _ \<guillemotright>_\<guillemotright> _" [65,65,65,65] 71)
 where
   Skip: "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
@@ -823,7 +823,7 @@
 ML_setup {*
 change_simpset (fn ss => ss delloop "split_all_tac");
 *}
-inductive_cases2 da_elim_cases [cases set]:
+inductive_cases da_elim_cases [cases set]:
   "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A" 
   "Env\<turnstile> B \<guillemotright>In1r Skip\<guillemotright> A" 
   "Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A"
diff -r a455e69c31cc -r b07cff284683 src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/Eval.thy	Wed Jul 11 11:16:34 2007 +0200
@@ -474,7 +474,7 @@
        
 section "evaluation judgments"
 
-inductive2
+inductive
   halloc :: "[prog,state,obj_tag,loc,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60) for G::prog
 where --{* allocating objects on the heap, cf. 12.5 *}
 
@@ -487,7 +487,7 @@
             \<Longrightarrow>
 	    G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"
 
-inductive2 sxalloc :: "[prog,state,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,61]60) for G::prog
+inductive sxalloc :: "[prog,state,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,61]60) for G::prog
 where --{* allocating exception objects for
   standard exceptions (other than OutOfMemory) *}
 
@@ -503,7 +503,7 @@
 	  G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
 
 
-inductive2
+inductive
   eval :: "[prog,state,term,vals,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> '(_, _')"  [61,61,80,0,0]60)
   and exec ::"[prog,state,stmt      ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _"   [61,61,65,   61]60)
   and evar ::"[prog,state,var  ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)
@@ -765,17 +765,17 @@
 
 declare split_if     [split del] split_if_asm     [split del] 
         option.split [split del] option.split_asm [split del]
-inductive_cases2 halloc_elim_cases: 
+inductive_cases halloc_elim_cases: 
   "G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
   "G\<turnstile>(Norm    s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
 
-inductive_cases2 sxalloc_elim_cases:
+inductive_cases sxalloc_elim_cases:
  	"G\<turnstile> Norm                 s  \<midarrow>sxalloc\<rightarrow> s'"
         "G\<turnstile>(Some (Jump j),s) \<midarrow>sxalloc\<rightarrow> s'"
  	"G\<turnstile>(Some (Error e),s) \<midarrow>sxalloc\<rightarrow> s'"
         "G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'"
  	"G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'"
-inductive_cases2 sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
+inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
 
 lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';  
        \<And>s.   \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;  
@@ -793,9 +793,9 @@
 ML_setup {*
 change_simpset (fn ss => ss delloop "split_all_tac");
 *}
-inductive_cases2 eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')"
+inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')"
 
-inductive_cases2 eval_elim_cases [cases set]:
+inductive_cases eval_elim_cases [cases set]:
         "G\<turnstile>(Some xc,s) \<midarrow>t                              \<succ>\<rightarrow> (v, s')"
 	"G\<turnstile>Norm s \<midarrow>In1r Skip                           \<succ>\<rightarrow> (x, s')"
         "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                        \<succ>\<rightarrow> (x, s')"
diff -r a455e69c31cc -r b07cff284683 src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/Evaln.thy	Wed Jul 11 11:16:34 2007 +0200
@@ -28,7 +28,7 @@
 for welltyped, and definitely assigned terms.
 *}
 
-inductive2
+inductive
   evaln	:: "[prog, state, term, nat, vals, state] \<Rightarrow> bool"
     ("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> '(_, _')" [61,61,80,61,0,0] 60)
   and evarn :: "[prog, state, var, vvar, nat, state] \<Rightarrow> bool"
@@ -201,9 +201,9 @@
 ML_setup {*
 change_simpset (fn ss => ss delloop "split_all_tac");
 *}
-inductive_cases2 evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
+inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
 
-inductive_cases2 evaln_elim_cases:
+inductive_cases evaln_elim_cases:
 	"G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> (v, s')"
 	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> (x, s')"
         "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                   \<succ>\<midarrow>n\<rightarrow> (x, s')"
diff -r a455e69c31cc -r b07cff284683 src/HOL/Bali/Trans.thy
--- a/src/HOL/Bali/Trans.thy	Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/Trans.thy	Wed Jul 11 11:16:34 2007 +0200
@@ -68,7 +68,7 @@
   "Ref a" == "Lit (Addr a)"
   "SKIP"  == "Lit Unit"
 
-inductive2
+inductive
   step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
   for G :: prog
 where
diff -r a455e69c31cc -r b07cff284683 src/HOL/Bali/TypeRel.thy
--- a/src/HOL/Bali/TypeRel.thy	Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/TypeRel.thy	Wed Jul 11 11:16:34 2007 +0200
@@ -351,7 +351,7 @@
 done
 
 
-inductive2 --{* implementation, cf. 8.1.4 *}
+inductive --{* implementation, cf. 8.1.4 *}
   implmt :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70)
   for G :: prog
 where
@@ -385,7 +385,7 @@
 
 section "widening relation"
 
-inductive2
+inductive
  --{*widening, viz. method invocation conversion, cf. 5.3
 			    i.e. kind of syntactic subtyping *}
   widen :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>_" [71,71,71] 70)
@@ -407,14 +407,14 @@
 lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x"
 *)
 lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> (\<exists>y. T = PrimT y)"
-apply (ind_cases2 "G\<turnstile>PrimT x\<preceq>T")
+apply (ind_cases "G\<turnstile>PrimT x\<preceq>T")
 by auto
 
 (* too strong in general:
 lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x"
 *)
 lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> \<exists>y. S = PrimT y"
-apply (ind_cases2 "G\<turnstile>S\<preceq>PrimT x")
+apply (ind_cases "G\<turnstile>S\<preceq>PrimT x")
 by auto
 
 text {* 
@@ -424,37 +424,37 @@
  *}
 
 lemma widen_PrimT_strong: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x"
-by (ind_cases2 "G\<turnstile>PrimT x\<preceq>T") simp_all
+by (ind_cases "G\<turnstile>PrimT x\<preceq>T") simp_all
 
 lemma widen_PrimT2_strong: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x"
-by (ind_cases2 "G\<turnstile>S\<preceq>PrimT x") simp_all
+by (ind_cases "G\<turnstile>S\<preceq>PrimT x") simp_all
 
 text {* Specialized versions for booleans also would work for real Java *}
 
 lemma widen_Boolean: "G\<turnstile>PrimT Boolean\<preceq>T \<Longrightarrow> T = PrimT Boolean"
-by (ind_cases2 "G\<turnstile>PrimT Boolean\<preceq>T") simp_all
+by (ind_cases "G\<turnstile>PrimT Boolean\<preceq>T") simp_all
 
 lemma widen_Boolean2: "G\<turnstile>S\<preceq>PrimT Boolean \<Longrightarrow> S = PrimT Boolean"
-by (ind_cases2 "G\<turnstile>S\<preceq>PrimT Boolean") simp_all
+by (ind_cases "G\<turnstile>S\<preceq>PrimT Boolean") simp_all
 
 lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T \<Longrightarrow> \<exists>t. T=RefT t"
-apply (ind_cases2 "G\<turnstile>RefT R\<preceq>T")
+apply (ind_cases "G\<turnstile>RefT R\<preceq>T")
 by auto
 
 lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R \<Longrightarrow> \<exists>t. S=RefT t"
-apply (ind_cases2 "G\<turnstile>S\<preceq>RefT R")
+apply (ind_cases "G\<turnstile>S\<preceq>RefT R")
 by auto
 
 lemma widen_Iface: "G\<turnstile>Iface I\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>J. T=Iface J)"
-apply (ind_cases2 "G\<turnstile>Iface I\<preceq>T")
+apply (ind_cases "G\<turnstile>Iface I\<preceq>T")
 by auto
 
 lemma widen_Iface2: "G\<turnstile>S\<preceq> Iface J \<Longrightarrow> S = NT \<or> (\<exists>I. S = Iface I) \<or> (\<exists>D. S = Class D)"
-apply (ind_cases2 "G\<turnstile>S\<preceq> Iface J")
+apply (ind_cases "G\<turnstile>S\<preceq> Iface J")
 by auto
 
 lemma widen_Iface_Iface: "G\<turnstile>Iface I\<preceq> Iface J \<Longrightarrow> G\<turnstile>I\<preceq>I J"
-apply (ind_cases2 "G\<turnstile>Iface I\<preceq> Iface J")
+apply (ind_cases "G\<turnstile>Iface I\<preceq> Iface J")
 by auto
 
 lemma widen_Iface_Iface_eq [simp]: "G\<turnstile>Iface I\<preceq> Iface J = G\<turnstile>I\<preceq>I J"
@@ -464,15 +464,15 @@
 done
 
 lemma widen_Class: "G\<turnstile>Class C\<preceq>T \<Longrightarrow>  (\<exists>D. T=Class D) \<or> (\<exists>I. T=Iface I)"
-apply (ind_cases2 "G\<turnstile>Class C\<preceq>T")
+apply (ind_cases "G\<turnstile>Class C\<preceq>T")
 by auto
 
 lemma widen_Class2: "G\<turnstile>S\<preceq> Class C \<Longrightarrow> C = Object \<or> S = NT \<or> (\<exists>D. S = Class D)"
-apply (ind_cases2 "G\<turnstile>S\<preceq> Class C")
+apply (ind_cases "G\<turnstile>S\<preceq> Class C")
 by auto
 
 lemma widen_Class_Class: "G\<turnstile>Class C\<preceq> Class cm \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C cm"
-apply (ind_cases2 "G\<turnstile>Class C\<preceq> Class cm")
+apply (ind_cases "G\<turnstile>Class C\<preceq> Class cm")
 by auto
 
 lemma widen_Class_Class_eq [simp]: "G\<turnstile>Class C\<preceq> Class cm = G\<turnstile>C\<preceq>\<^sub>C cm"
@@ -482,7 +482,7 @@
 done
 
 lemma widen_Class_Iface: "G\<turnstile>Class C\<preceq> Iface I \<Longrightarrow> G\<turnstile>C\<leadsto>I"
-apply (ind_cases2 "G\<turnstile>Class C\<preceq> Iface I")
+apply (ind_cases "G\<turnstile>Class C\<preceq> Iface I")
 by auto
 
 lemma widen_Class_Iface_eq [simp]: "G\<turnstile>Class C\<preceq> Iface I = G\<turnstile>C\<leadsto>I"
@@ -492,21 +492,21 @@
 done
 
 lemma widen_Array: "G\<turnstile>S.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>T'. T=T'.[] \<and> G\<turnstile>S\<preceq>T')"
-apply (ind_cases2 "G\<turnstile>S.[]\<preceq>T")
+apply (ind_cases "G\<turnstile>S.[]\<preceq>T")
 by auto
 
 lemma widen_Array2: "G\<turnstile>S\<preceq>T.[] \<Longrightarrow> S = NT \<or> (\<exists>S'. S=S'.[] \<and> G\<turnstile>S'\<preceq>T)"
-apply (ind_cases2 "G\<turnstile>S\<preceq>T.[]")
+apply (ind_cases "G\<turnstile>S\<preceq>T.[]")
 by auto
 
 
 lemma widen_ArrayPrimT: "G\<turnstile>PrimT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> T=PrimT t.[]"
-apply (ind_cases2 "G\<turnstile>PrimT t.[]\<preceq>T")
+apply (ind_cases "G\<turnstile>PrimT t.[]\<preceq>T")
 by auto
 
 lemma widen_ArrayRefT: 
   "G\<turnstile>RefT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>s. T=RefT s.[] \<and> G\<turnstile>RefT t\<preceq>RefT s)"
-apply (ind_cases2 "G\<turnstile>RefT t.[]\<preceq>T")
+apply (ind_cases "G\<turnstile>RefT t.[]\<preceq>T")
 by auto
 
 lemma widen_ArrayRefT_ArrayRefT_eq [simp]: 
@@ -527,7 +527,7 @@
 
 
 lemma widen_NT2: "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT"
-apply (ind_cases2 "G\<turnstile>S\<preceq>NT")
+apply (ind_cases "G\<turnstile>S\<preceq>NT")
 by auto
 
 lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object"
@@ -610,7 +610,7 @@
 *)
 
 (* more detailed than necessary for type-safety, see above rules. *)
-inductive2 --{* narrowing reference conversion, cf. 5.1.5 *}
+inductive --{* narrowing reference conversion, cf. 5.1.5 *}
   narrow :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<succ>_" [71,71,71] 70)
   for G :: prog
 where
@@ -625,20 +625,20 @@
 
 (*unused*)
 lemma narrow_RefT: "G\<turnstile>RefT R\<succ>T \<Longrightarrow> \<exists>t. T=RefT t"
-apply (ind_cases2 "G\<turnstile>RefT R\<succ>T")
+apply (ind_cases "G\<turnstile>RefT R\<succ>T")
 by auto
 
 lemma narrow_RefT2: "G\<turnstile>S\<succ>RefT R \<Longrightarrow> \<exists>t. S=RefT t"
-apply (ind_cases2 "G\<turnstile>S\<succ>RefT R")
+apply (ind_cases "G\<turnstile>S\<succ>RefT R")
 by auto
 
 (*unused*)
 lemma narrow_PrimT: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> \<exists>t. T=PrimT t"
-by (ind_cases2 "G\<turnstile>PrimT pt\<succ>T")
+by (ind_cases "G\<turnstile>PrimT pt\<succ>T")
 
 lemma narrow_PrimT2: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow>  
 				  \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
-by (ind_cases2 "G\<turnstile>S\<succ>PrimT pt")
+by (ind_cases "G\<turnstile>S\<succ>PrimT pt")
 
 text {* 
    These narrowing lemmata hold in Bali but are to strong for ordinary
@@ -646,22 +646,22 @@
    long, int. These lemmata are just for documentation and are not used.
  *}
 lemma narrow_PrimT_strong: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> T=PrimT pt"
-by (ind_cases2 "G\<turnstile>PrimT pt\<succ>T")
+by (ind_cases "G\<turnstile>PrimT pt\<succ>T")
 
 lemma narrow_PrimT2_strong: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow> S=PrimT pt"
-by (ind_cases2 "G\<turnstile>S\<succ>PrimT pt")
+by (ind_cases "G\<turnstile>S\<succ>PrimT pt")
 
 text {* Specialized versions for booleans also would work for real Java *}
 
 lemma narrow_Boolean: "G\<turnstile>PrimT Boolean\<succ>T \<Longrightarrow> T=PrimT Boolean"
-by (ind_cases2 "G\<turnstile>PrimT Boolean\<succ>T")
+by (ind_cases "G\<turnstile>PrimT Boolean\<succ>T")
 
 lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean \<Longrightarrow> S=PrimT Boolean"
-by (ind_cases2 "G\<turnstile>S\<succ>PrimT Boolean")
+by (ind_cases "G\<turnstile>S\<succ>PrimT Boolean")
 
 section "casting relation"
 
-inductive2 --{* casting conversion, cf. 5.5 *}
+inductive --{* casting conversion, cf. 5.5 *}
   cast :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70)
   for G :: prog
 where
@@ -670,20 +670,20 @@
 
 (*unused*)
 lemma cast_RefT: "G\<turnstile>RefT R\<preceq>? T \<Longrightarrow> \<exists>t. T=RefT t"
-apply (ind_cases2 "G\<turnstile>RefT R\<preceq>? T")
+apply (ind_cases "G\<turnstile>RefT R\<preceq>? T")
 by (auto dest: widen_RefT narrow_RefT)
 
 lemma cast_RefT2: "G\<turnstile>S\<preceq>? RefT R \<Longrightarrow> \<exists>t. S=RefT t"
-apply (ind_cases2 "G\<turnstile>S\<preceq>? RefT R")
+apply (ind_cases "G\<turnstile>S\<preceq>? RefT R")
 by (auto dest: widen_RefT2 narrow_RefT2)
 
 (*unused*)
 lemma cast_PrimT: "G\<turnstile>PrimT pt\<preceq>? T \<Longrightarrow> \<exists>t. T=PrimT t"
-apply (ind_cases2 "G\<turnstile>PrimT pt\<preceq>? T")
+apply (ind_cases "G\<turnstile>PrimT pt\<preceq>? T")
 by (auto dest: widen_PrimT narrow_PrimT)
 
 lemma cast_PrimT2: "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
-apply (ind_cases2 "G\<turnstile>S\<preceq>? PrimT pt")
+apply (ind_cases "G\<turnstile>S\<preceq>? PrimT pt")
 by (auto dest: widen_PrimT2 narrow_PrimT2)
 
 lemma cast_Boolean: 
diff -r a455e69c31cc -r b07cff284683 src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/WellType.thy	Wed Jul 11 11:16:34 2007 +0200
@@ -246,7 +246,7 @@
   "tys"   <= (type) "ty + ty list"
 
 
-inductive2 
+inductive
   wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
   and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
   and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
@@ -456,7 +456,7 @@
 change_simpset (fn ss => ss delloop "split_all_tac")
 *}
 
-inductive_cases2 wt_elim_cases [cases set]:
+inductive_cases wt_elim_cases [cases set]:
 	"E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
 	"E,dt\<Turnstile>In2  ({accC,statDeclC,s}e..fn)\<Colon>T"
 	"E,dt\<Turnstile>In2  (e.[i])                 \<Colon>T"
diff -r a455e69c31cc -r b07cff284683 src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Extraction/Higman.thy	Wed Jul 11 11:16:34 2007 +0200
@@ -15,37 +15,37 @@
 
 datatype letter = A | B
 
-inductive2 emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"
+inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"
 where
    emb0 [Pure.intro]: "emb [] bs"
  | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)"
  | emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)"
 
-inductive2 L :: "letter list \<Rightarrow> letter list list \<Rightarrow> bool"
+inductive L :: "letter list \<Rightarrow> letter list list \<Rightarrow> bool"
   for v :: "letter list"
 where
    L0 [Pure.intro]: "emb w v \<Longrightarrow> L v (w # ws)"
  | L1 [Pure.intro]: "L v ws \<Longrightarrow> L v (w # ws)"
 
-inductive2 good :: "letter list list \<Rightarrow> bool"
+inductive good :: "letter list list \<Rightarrow> bool"
 where
     good0 [Pure.intro]: "L w ws \<Longrightarrow> good (w # ws)"
   | good1 [Pure.intro]: "good ws \<Longrightarrow> good (w # ws)"
 
-inductive2 R :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
+inductive R :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
   for a :: letter
 where
     R0 [Pure.intro]: "R a [] []"
   | R1 [Pure.intro]: "R a vs ws \<Longrightarrow> R a (w # vs) ((a # w) # ws)"
 
-inductive2 T :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
+inductive T :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
   for a :: letter
 where
     T0 [Pure.intro]: "a \<noteq> b \<Longrightarrow> R b ws zs \<Longrightarrow> T a (w # zs) ((a # w) # zs)"
   | T1 [Pure.intro]: "T a ws zs \<Longrightarrow> T a (w # ws) ((a # w) # zs)"
   | T2 [Pure.intro]: "a \<noteq> b \<Longrightarrow> T a ws zs \<Longrightarrow> T a ws ((b # w) # zs)"
 
-inductive2 bar :: "letter list list \<Rightarrow> bool"
+inductive bar :: "letter list list \<Rightarrow> bool"
 where
     bar1 [Pure.intro]: "good ws \<Longrightarrow> bar ws"
   | bar2 [Pure.intro]: "(\<And>w. bar (w # ws)) \<Longrightarrow> bar ws"