Renamed inductive2 to inductive.
authorberghofe
Wed Jul 11 11:16:34 2007 +0200 (2007-07-11)
changeset 23747b07cff284683
parent 23746 a455e69c31cc
child 23748 1ff6b562076f
Renamed inductive2 to inductive.
src/HOL/Bali/AxSem.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/DefiniteAssignment.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/Trans.thy
src/HOL/Bali/TypeRel.thy
src/HOL/Bali/WellType.thy
src/HOL/Extraction/Higman.thy
     1.1 --- a/src/HOL/Bali/AxSem.thy	Wed Jul 11 11:14:51 2007 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Wed Jul 11 11:16:34 2007 +0200
     1.3 @@ -476,7 +476,7 @@
     1.4  change_claset (fn cs => cs delSWrapper "split_all_tac");
     1.5  *}
     1.6  
     1.7 -inductive2
     1.8 +inductive
     1.9    ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57)
    1.10    and ax_deriv :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triple  \<Rightarrow> bool" ("_,_\<turnstile>_" [61,58,58] 57)
    1.11    for G :: prog
     2.1 --- a/src/HOL/Bali/DeclConcepts.thy	Wed Jul 11 11:14:51 2007 +0200
     2.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Wed Jul 11 11:16:34 2007 +0200
     2.3 @@ -541,7 +541,7 @@
     2.4     below
     2.5  *)
     2.6  
     2.7 -inductive2
     2.8 +inductive
     2.9    members :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
    2.10      ("_ \<turnstile> _ member'_of _" [61,61,61] 60)
    2.11    for G :: prog
    2.12 @@ -634,7 +634,7 @@
    2.13  
    2.14  text {* Static overriding (used during the typecheck of the compiler) *}
    2.15  
    2.16 -inductive2
    2.17 +inductive
    2.18    stat_overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
    2.19      ("_ \<turnstile> _ overrides\<^sub>S _" [61,61,61] 60)
    2.20    for G :: prog
    2.21 @@ -653,7 +653,7 @@
    2.22  
    2.23  text {* Dynamic overriding (used during the typecheck of the compiler) *}
    2.24  
    2.25 -inductive2
    2.26 +inductive
    2.27    overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
    2.28      ("_ \<turnstile> _ overrides _" [61,61,61] 60)
    2.29    for G :: prog
    2.30 @@ -784,7 +784,7 @@
    2.31  \end{itemize} 
    2.32  *} 
    2.33  
    2.34 -inductive2
    2.35 +inductive
    2.36    accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
    2.37    and accessible_from :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
    2.38      ("_ \<turnstile> _ of _ accessible'_from _" [61,61,61,61] 60)
    2.39 @@ -828,7 +828,7 @@
    2.40  "G\<turnstile>Field fn f of C accessible_from accclass"  
    2.41   \<rightleftharpoons> "G\<turnstile>(fieldm fn f) of C accessible_from accclass" 
    2.42  
    2.43 -inductive2
    2.44 +inductive
    2.45    dyn_accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
    2.46    and dyn_accessible_from' ::  "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
    2.47      ("_ \<turnstile> _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
     3.1 --- a/src/HOL/Bali/DefiniteAssignment.thy	Wed Jul 11 11:14:51 2007 +0200
     3.2 +++ b/src/HOL/Bali/DefiniteAssignment.thy	Wed Jul 11 11:16:34 2007 +0200
     3.3 @@ -533,7 +533,7 @@
     3.4  distinguish boolean and other expressions.
     3.5  *}
     3.6  
     3.7 -inductive2
     3.8 +inductive
     3.9    da :: "env \<Rightarrow> lname set \<Rightarrow> term \<Rightarrow> assigned \<Rightarrow> bool" ("_\<turnstile> _ \<guillemotright>_\<guillemotright> _" [65,65,65,65] 71)
    3.10  where
    3.11    Skip: "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
    3.12 @@ -823,7 +823,7 @@
    3.13  ML_setup {*
    3.14  change_simpset (fn ss => ss delloop "split_all_tac");
    3.15  *}
    3.16 -inductive_cases2 da_elim_cases [cases set]:
    3.17 +inductive_cases da_elim_cases [cases set]:
    3.18    "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A" 
    3.19    "Env\<turnstile> B \<guillemotright>In1r Skip\<guillemotright> A" 
    3.20    "Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A"
     4.1 --- a/src/HOL/Bali/Eval.thy	Wed Jul 11 11:14:51 2007 +0200
     4.2 +++ b/src/HOL/Bali/Eval.thy	Wed Jul 11 11:16:34 2007 +0200
     4.3 @@ -474,7 +474,7 @@
     4.4         
     4.5  section "evaluation judgments"
     4.6  
     4.7 -inductive2
     4.8 +inductive
     4.9    halloc :: "[prog,state,obj_tag,loc,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60) for G::prog
    4.10  where --{* allocating objects on the heap, cf. 12.5 *}
    4.11  
    4.12 @@ -487,7 +487,7 @@
    4.13              \<Longrightarrow>
    4.14  	    G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"
    4.15  
    4.16 -inductive2 sxalloc :: "[prog,state,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,61]60) for G::prog
    4.17 +inductive sxalloc :: "[prog,state,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,61]60) for G::prog
    4.18  where --{* allocating exception objects for
    4.19    standard exceptions (other than OutOfMemory) *}
    4.20  
    4.21 @@ -503,7 +503,7 @@
    4.22  	  G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
    4.23  
    4.24  
    4.25 -inductive2
    4.26 +inductive
    4.27    eval :: "[prog,state,term,vals,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> '(_, _')"  [61,61,80,0,0]60)
    4.28    and exec ::"[prog,state,stmt      ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _"   [61,61,65,   61]60)
    4.29    and evar ::"[prog,state,var  ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)
    4.30 @@ -765,17 +765,17 @@
    4.31  
    4.32  declare split_if     [split del] split_if_asm     [split del] 
    4.33          option.split [split del] option.split_asm [split del]
    4.34 -inductive_cases2 halloc_elim_cases: 
    4.35 +inductive_cases halloc_elim_cases: 
    4.36    "G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
    4.37    "G\<turnstile>(Norm    s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
    4.38  
    4.39 -inductive_cases2 sxalloc_elim_cases:
    4.40 +inductive_cases sxalloc_elim_cases:
    4.41   	"G\<turnstile> Norm                 s  \<midarrow>sxalloc\<rightarrow> s'"
    4.42          "G\<turnstile>(Some (Jump j),s) \<midarrow>sxalloc\<rightarrow> s'"
    4.43   	"G\<turnstile>(Some (Error e),s) \<midarrow>sxalloc\<rightarrow> s'"
    4.44          "G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'"
    4.45   	"G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'"
    4.46 -inductive_cases2 sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
    4.47 +inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
    4.48  
    4.49  lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';  
    4.50         \<And>s.   \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;  
    4.51 @@ -793,9 +793,9 @@
    4.52  ML_setup {*
    4.53  change_simpset (fn ss => ss delloop "split_all_tac");
    4.54  *}
    4.55 -inductive_cases2 eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')"
    4.56 +inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')"
    4.57  
    4.58 -inductive_cases2 eval_elim_cases [cases set]:
    4.59 +inductive_cases eval_elim_cases [cases set]:
    4.60          "G\<turnstile>(Some xc,s) \<midarrow>t                              \<succ>\<rightarrow> (v, s')"
    4.61  	"G\<turnstile>Norm s \<midarrow>In1r Skip                           \<succ>\<rightarrow> (x, s')"
    4.62          "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                        \<succ>\<rightarrow> (x, s')"
     5.1 --- a/src/HOL/Bali/Evaln.thy	Wed Jul 11 11:14:51 2007 +0200
     5.2 +++ b/src/HOL/Bali/Evaln.thy	Wed Jul 11 11:16:34 2007 +0200
     5.3 @@ -28,7 +28,7 @@
     5.4  for welltyped, and definitely assigned terms.
     5.5  *}
     5.6  
     5.7 -inductive2
     5.8 +inductive
     5.9    evaln	:: "[prog, state, term, nat, vals, state] \<Rightarrow> bool"
    5.10      ("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> '(_, _')" [61,61,80,61,0,0] 60)
    5.11    and evarn :: "[prog, state, var, vvar, nat, state] \<Rightarrow> bool"
    5.12 @@ -201,9 +201,9 @@
    5.13  ML_setup {*
    5.14  change_simpset (fn ss => ss delloop "split_all_tac");
    5.15  *}
    5.16 -inductive_cases2 evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
    5.17 +inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
    5.18  
    5.19 -inductive_cases2 evaln_elim_cases:
    5.20 +inductive_cases evaln_elim_cases:
    5.21  	"G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> (v, s')"
    5.22  	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> (x, s')"
    5.23          "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                   \<succ>\<midarrow>n\<rightarrow> (x, s')"
     6.1 --- a/src/HOL/Bali/Trans.thy	Wed Jul 11 11:14:51 2007 +0200
     6.2 +++ b/src/HOL/Bali/Trans.thy	Wed Jul 11 11:16:34 2007 +0200
     6.3 @@ -68,7 +68,7 @@
     6.4    "Ref a" == "Lit (Addr a)"
     6.5    "SKIP"  == "Lit Unit"
     6.6  
     6.7 -inductive2
     6.8 +inductive
     6.9    step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
    6.10    for G :: prog
    6.11  where
     7.1 --- a/src/HOL/Bali/TypeRel.thy	Wed Jul 11 11:14:51 2007 +0200
     7.2 +++ b/src/HOL/Bali/TypeRel.thy	Wed Jul 11 11:16:34 2007 +0200
     7.3 @@ -351,7 +351,7 @@
     7.4  done
     7.5  
     7.6  
     7.7 -inductive2 --{* implementation, cf. 8.1.4 *}
     7.8 +inductive --{* implementation, cf. 8.1.4 *}
     7.9    implmt :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70)
    7.10    for G :: prog
    7.11  where
    7.12 @@ -385,7 +385,7 @@
    7.13  
    7.14  section "widening relation"
    7.15  
    7.16 -inductive2
    7.17 +inductive
    7.18   --{*widening, viz. method invocation conversion, cf. 5.3
    7.19  			    i.e. kind of syntactic subtyping *}
    7.20    widen :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>_" [71,71,71] 70)
    7.21 @@ -407,14 +407,14 @@
    7.22  lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x"
    7.23  *)
    7.24  lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> (\<exists>y. T = PrimT y)"
    7.25 -apply (ind_cases2 "G\<turnstile>PrimT x\<preceq>T")
    7.26 +apply (ind_cases "G\<turnstile>PrimT x\<preceq>T")
    7.27  by auto
    7.28  
    7.29  (* too strong in general:
    7.30  lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x"
    7.31  *)
    7.32  lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> \<exists>y. S = PrimT y"
    7.33 -apply (ind_cases2 "G\<turnstile>S\<preceq>PrimT x")
    7.34 +apply (ind_cases "G\<turnstile>S\<preceq>PrimT x")
    7.35  by auto
    7.36  
    7.37  text {* 
    7.38 @@ -424,37 +424,37 @@
    7.39   *}
    7.40  
    7.41  lemma widen_PrimT_strong: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x"
    7.42 -by (ind_cases2 "G\<turnstile>PrimT x\<preceq>T") simp_all
    7.43 +by (ind_cases "G\<turnstile>PrimT x\<preceq>T") simp_all
    7.44  
    7.45  lemma widen_PrimT2_strong: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x"
    7.46 -by (ind_cases2 "G\<turnstile>S\<preceq>PrimT x") simp_all
    7.47 +by (ind_cases "G\<turnstile>S\<preceq>PrimT x") simp_all
    7.48  
    7.49  text {* Specialized versions for booleans also would work for real Java *}
    7.50  
    7.51  lemma widen_Boolean: "G\<turnstile>PrimT Boolean\<preceq>T \<Longrightarrow> T = PrimT Boolean"
    7.52 -by (ind_cases2 "G\<turnstile>PrimT Boolean\<preceq>T") simp_all
    7.53 +by (ind_cases "G\<turnstile>PrimT Boolean\<preceq>T") simp_all
    7.54  
    7.55  lemma widen_Boolean2: "G\<turnstile>S\<preceq>PrimT Boolean \<Longrightarrow> S = PrimT Boolean"
    7.56 -by (ind_cases2 "G\<turnstile>S\<preceq>PrimT Boolean") simp_all
    7.57 +by (ind_cases "G\<turnstile>S\<preceq>PrimT Boolean") simp_all
    7.58  
    7.59  lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T \<Longrightarrow> \<exists>t. T=RefT t"
    7.60 -apply (ind_cases2 "G\<turnstile>RefT R\<preceq>T")
    7.61 +apply (ind_cases "G\<turnstile>RefT R\<preceq>T")
    7.62  by auto
    7.63  
    7.64  lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R \<Longrightarrow> \<exists>t. S=RefT t"
    7.65 -apply (ind_cases2 "G\<turnstile>S\<preceq>RefT R")
    7.66 +apply (ind_cases "G\<turnstile>S\<preceq>RefT R")
    7.67  by auto
    7.68  
    7.69  lemma widen_Iface: "G\<turnstile>Iface I\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>J. T=Iface J)"
    7.70 -apply (ind_cases2 "G\<turnstile>Iface I\<preceq>T")
    7.71 +apply (ind_cases "G\<turnstile>Iface I\<preceq>T")
    7.72  by auto
    7.73  
    7.74  lemma widen_Iface2: "G\<turnstile>S\<preceq> Iface J \<Longrightarrow> S = NT \<or> (\<exists>I. S = Iface I) \<or> (\<exists>D. S = Class D)"
    7.75 -apply (ind_cases2 "G\<turnstile>S\<preceq> Iface J")
    7.76 +apply (ind_cases "G\<turnstile>S\<preceq> Iface J")
    7.77  by auto
    7.78  
    7.79  lemma widen_Iface_Iface: "G\<turnstile>Iface I\<preceq> Iface J \<Longrightarrow> G\<turnstile>I\<preceq>I J"
    7.80 -apply (ind_cases2 "G\<turnstile>Iface I\<preceq> Iface J")
    7.81 +apply (ind_cases "G\<turnstile>Iface I\<preceq> Iface J")
    7.82  by auto
    7.83  
    7.84  lemma widen_Iface_Iface_eq [simp]: "G\<turnstile>Iface I\<preceq> Iface J = G\<turnstile>I\<preceq>I J"
    7.85 @@ -464,15 +464,15 @@
    7.86  done
    7.87  
    7.88  lemma widen_Class: "G\<turnstile>Class C\<preceq>T \<Longrightarrow>  (\<exists>D. T=Class D) \<or> (\<exists>I. T=Iface I)"
    7.89 -apply (ind_cases2 "G\<turnstile>Class C\<preceq>T")
    7.90 +apply (ind_cases "G\<turnstile>Class C\<preceq>T")
    7.91  by auto
    7.92  
    7.93  lemma widen_Class2: "G\<turnstile>S\<preceq> Class C \<Longrightarrow> C = Object \<or> S = NT \<or> (\<exists>D. S = Class D)"
    7.94 -apply (ind_cases2 "G\<turnstile>S\<preceq> Class C")
    7.95 +apply (ind_cases "G\<turnstile>S\<preceq> Class C")
    7.96  by auto
    7.97  
    7.98  lemma widen_Class_Class: "G\<turnstile>Class C\<preceq> Class cm \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C cm"
    7.99 -apply (ind_cases2 "G\<turnstile>Class C\<preceq> Class cm")
   7.100 +apply (ind_cases "G\<turnstile>Class C\<preceq> Class cm")
   7.101  by auto
   7.102  
   7.103  lemma widen_Class_Class_eq [simp]: "G\<turnstile>Class C\<preceq> Class cm = G\<turnstile>C\<preceq>\<^sub>C cm"
   7.104 @@ -482,7 +482,7 @@
   7.105  done
   7.106  
   7.107  lemma widen_Class_Iface: "G\<turnstile>Class C\<preceq> Iface I \<Longrightarrow> G\<turnstile>C\<leadsto>I"
   7.108 -apply (ind_cases2 "G\<turnstile>Class C\<preceq> Iface I")
   7.109 +apply (ind_cases "G\<turnstile>Class C\<preceq> Iface I")
   7.110  by auto
   7.111  
   7.112  lemma widen_Class_Iface_eq [simp]: "G\<turnstile>Class C\<preceq> Iface I = G\<turnstile>C\<leadsto>I"
   7.113 @@ -492,21 +492,21 @@
   7.114  done
   7.115  
   7.116  lemma widen_Array: "G\<turnstile>S.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>T'. T=T'.[] \<and> G\<turnstile>S\<preceq>T')"
   7.117 -apply (ind_cases2 "G\<turnstile>S.[]\<preceq>T")
   7.118 +apply (ind_cases "G\<turnstile>S.[]\<preceq>T")
   7.119  by auto
   7.120  
   7.121  lemma widen_Array2: "G\<turnstile>S\<preceq>T.[] \<Longrightarrow> S = NT \<or> (\<exists>S'. S=S'.[] \<and> G\<turnstile>S'\<preceq>T)"
   7.122 -apply (ind_cases2 "G\<turnstile>S\<preceq>T.[]")
   7.123 +apply (ind_cases "G\<turnstile>S\<preceq>T.[]")
   7.124  by auto
   7.125  
   7.126  
   7.127  lemma widen_ArrayPrimT: "G\<turnstile>PrimT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> T=PrimT t.[]"
   7.128 -apply (ind_cases2 "G\<turnstile>PrimT t.[]\<preceq>T")
   7.129 +apply (ind_cases "G\<turnstile>PrimT t.[]\<preceq>T")
   7.130  by auto
   7.131  
   7.132  lemma widen_ArrayRefT: 
   7.133    "G\<turnstile>RefT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>s. T=RefT s.[] \<and> G\<turnstile>RefT t\<preceq>RefT s)"
   7.134 -apply (ind_cases2 "G\<turnstile>RefT t.[]\<preceq>T")
   7.135 +apply (ind_cases "G\<turnstile>RefT t.[]\<preceq>T")
   7.136  by auto
   7.137  
   7.138  lemma widen_ArrayRefT_ArrayRefT_eq [simp]: 
   7.139 @@ -527,7 +527,7 @@
   7.140  
   7.141  
   7.142  lemma widen_NT2: "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT"
   7.143 -apply (ind_cases2 "G\<turnstile>S\<preceq>NT")
   7.144 +apply (ind_cases "G\<turnstile>S\<preceq>NT")
   7.145  by auto
   7.146  
   7.147  lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object"
   7.148 @@ -610,7 +610,7 @@
   7.149  *)
   7.150  
   7.151  (* more detailed than necessary for type-safety, see above rules. *)
   7.152 -inductive2 --{* narrowing reference conversion, cf. 5.1.5 *}
   7.153 +inductive --{* narrowing reference conversion, cf. 5.1.5 *}
   7.154    narrow :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<succ>_" [71,71,71] 70)
   7.155    for G :: prog
   7.156  where
   7.157 @@ -625,20 +625,20 @@
   7.158  
   7.159  (*unused*)
   7.160  lemma narrow_RefT: "G\<turnstile>RefT R\<succ>T \<Longrightarrow> \<exists>t. T=RefT t"
   7.161 -apply (ind_cases2 "G\<turnstile>RefT R\<succ>T")
   7.162 +apply (ind_cases "G\<turnstile>RefT R\<succ>T")
   7.163  by auto
   7.164  
   7.165  lemma narrow_RefT2: "G\<turnstile>S\<succ>RefT R \<Longrightarrow> \<exists>t. S=RefT t"
   7.166 -apply (ind_cases2 "G\<turnstile>S\<succ>RefT R")
   7.167 +apply (ind_cases "G\<turnstile>S\<succ>RefT R")
   7.168  by auto
   7.169  
   7.170  (*unused*)
   7.171  lemma narrow_PrimT: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> \<exists>t. T=PrimT t"
   7.172 -by (ind_cases2 "G\<turnstile>PrimT pt\<succ>T")
   7.173 +by (ind_cases "G\<turnstile>PrimT pt\<succ>T")
   7.174  
   7.175  lemma narrow_PrimT2: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow>  
   7.176  				  \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
   7.177 -by (ind_cases2 "G\<turnstile>S\<succ>PrimT pt")
   7.178 +by (ind_cases "G\<turnstile>S\<succ>PrimT pt")
   7.179  
   7.180  text {* 
   7.181     These narrowing lemmata hold in Bali but are to strong for ordinary
   7.182 @@ -646,22 +646,22 @@
   7.183     long, int. These lemmata are just for documentation and are not used.
   7.184   *}
   7.185  lemma narrow_PrimT_strong: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> T=PrimT pt"
   7.186 -by (ind_cases2 "G\<turnstile>PrimT pt\<succ>T")
   7.187 +by (ind_cases "G\<turnstile>PrimT pt\<succ>T")
   7.188  
   7.189  lemma narrow_PrimT2_strong: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow> S=PrimT pt"
   7.190 -by (ind_cases2 "G\<turnstile>S\<succ>PrimT pt")
   7.191 +by (ind_cases "G\<turnstile>S\<succ>PrimT pt")
   7.192  
   7.193  text {* Specialized versions for booleans also would work for real Java *}
   7.194  
   7.195  lemma narrow_Boolean: "G\<turnstile>PrimT Boolean\<succ>T \<Longrightarrow> T=PrimT Boolean"
   7.196 -by (ind_cases2 "G\<turnstile>PrimT Boolean\<succ>T")
   7.197 +by (ind_cases "G\<turnstile>PrimT Boolean\<succ>T")
   7.198  
   7.199  lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean \<Longrightarrow> S=PrimT Boolean"
   7.200 -by (ind_cases2 "G\<turnstile>S\<succ>PrimT Boolean")
   7.201 +by (ind_cases "G\<turnstile>S\<succ>PrimT Boolean")
   7.202  
   7.203  section "casting relation"
   7.204  
   7.205 -inductive2 --{* casting conversion, cf. 5.5 *}
   7.206 +inductive --{* casting conversion, cf. 5.5 *}
   7.207    cast :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70)
   7.208    for G :: prog
   7.209  where
   7.210 @@ -670,20 +670,20 @@
   7.211  
   7.212  (*unused*)
   7.213  lemma cast_RefT: "G\<turnstile>RefT R\<preceq>? T \<Longrightarrow> \<exists>t. T=RefT t"
   7.214 -apply (ind_cases2 "G\<turnstile>RefT R\<preceq>? T")
   7.215 +apply (ind_cases "G\<turnstile>RefT R\<preceq>? T")
   7.216  by (auto dest: widen_RefT narrow_RefT)
   7.217  
   7.218  lemma cast_RefT2: "G\<turnstile>S\<preceq>? RefT R \<Longrightarrow> \<exists>t. S=RefT t"
   7.219 -apply (ind_cases2 "G\<turnstile>S\<preceq>? RefT R")
   7.220 +apply (ind_cases "G\<turnstile>S\<preceq>? RefT R")
   7.221  by (auto dest: widen_RefT2 narrow_RefT2)
   7.222  
   7.223  (*unused*)
   7.224  lemma cast_PrimT: "G\<turnstile>PrimT pt\<preceq>? T \<Longrightarrow> \<exists>t. T=PrimT t"
   7.225 -apply (ind_cases2 "G\<turnstile>PrimT pt\<preceq>? T")
   7.226 +apply (ind_cases "G\<turnstile>PrimT pt\<preceq>? T")
   7.227  by (auto dest: widen_PrimT narrow_PrimT)
   7.228  
   7.229  lemma cast_PrimT2: "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
   7.230 -apply (ind_cases2 "G\<turnstile>S\<preceq>? PrimT pt")
   7.231 +apply (ind_cases "G\<turnstile>S\<preceq>? PrimT pt")
   7.232  by (auto dest: widen_PrimT2 narrow_PrimT2)
   7.233  
   7.234  lemma cast_Boolean: 
     8.1 --- a/src/HOL/Bali/WellType.thy	Wed Jul 11 11:14:51 2007 +0200
     8.2 +++ b/src/HOL/Bali/WellType.thy	Wed Jul 11 11:16:34 2007 +0200
     8.3 @@ -246,7 +246,7 @@
     8.4    "tys"   <= (type) "ty + ty list"
     8.5  
     8.6  
     8.7 -inductive2 
     8.8 +inductive
     8.9    wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
    8.10    and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
    8.11    and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
    8.12 @@ -456,7 +456,7 @@
    8.13  change_simpset (fn ss => ss delloop "split_all_tac")
    8.14  *}
    8.15  
    8.16 -inductive_cases2 wt_elim_cases [cases set]:
    8.17 +inductive_cases wt_elim_cases [cases set]:
    8.18  	"E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
    8.19  	"E,dt\<Turnstile>In2  ({accC,statDeclC,s}e..fn)\<Colon>T"
    8.20  	"E,dt\<Turnstile>In2  (e.[i])                 \<Colon>T"
     9.1 --- a/src/HOL/Extraction/Higman.thy	Wed Jul 11 11:14:51 2007 +0200
     9.2 +++ b/src/HOL/Extraction/Higman.thy	Wed Jul 11 11:16:34 2007 +0200
     9.3 @@ -15,37 +15,37 @@
     9.4  
     9.5  datatype letter = A | B
     9.6  
     9.7 -inductive2 emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"
     9.8 +inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"
     9.9  where
    9.10     emb0 [Pure.intro]: "emb [] bs"
    9.11   | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)"
    9.12   | emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)"
    9.13  
    9.14 -inductive2 L :: "letter list \<Rightarrow> letter list list \<Rightarrow> bool"
    9.15 +inductive L :: "letter list \<Rightarrow> letter list list \<Rightarrow> bool"
    9.16    for v :: "letter list"
    9.17  where
    9.18     L0 [Pure.intro]: "emb w v \<Longrightarrow> L v (w # ws)"
    9.19   | L1 [Pure.intro]: "L v ws \<Longrightarrow> L v (w # ws)"
    9.20  
    9.21 -inductive2 good :: "letter list list \<Rightarrow> bool"
    9.22 +inductive good :: "letter list list \<Rightarrow> bool"
    9.23  where
    9.24      good0 [Pure.intro]: "L w ws \<Longrightarrow> good (w # ws)"
    9.25    | good1 [Pure.intro]: "good ws \<Longrightarrow> good (w # ws)"
    9.26  
    9.27 -inductive2 R :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
    9.28 +inductive R :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
    9.29    for a :: letter
    9.30  where
    9.31      R0 [Pure.intro]: "R a [] []"
    9.32    | R1 [Pure.intro]: "R a vs ws \<Longrightarrow> R a (w # vs) ((a # w) # ws)"
    9.33  
    9.34 -inductive2 T :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
    9.35 +inductive T :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
    9.36    for a :: letter
    9.37  where
    9.38      T0 [Pure.intro]: "a \<noteq> b \<Longrightarrow> R b ws zs \<Longrightarrow> T a (w # zs) ((a # w) # zs)"
    9.39    | T1 [Pure.intro]: "T a ws zs \<Longrightarrow> T a (w # ws) ((a # w) # zs)"
    9.40    | T2 [Pure.intro]: "a \<noteq> b \<Longrightarrow> T a ws zs \<Longrightarrow> T a ws ((b # w) # zs)"
    9.41  
    9.42 -inductive2 bar :: "letter list list \<Rightarrow> bool"
    9.43 +inductive bar :: "letter list list \<Rightarrow> bool"
    9.44  where
    9.45      bar1 [Pure.intro]: "good ws \<Longrightarrow> bar ws"
    9.46    | bar2 [Pure.intro]: "(\<And>w. bar (w # ws)) \<Longrightarrow> bar ws"