src/HOL/Bali/DeclConcepts.thy
changeset 23747 b07cff284683
parent 22426 1c38ca2496c4
child 24038 18182c4aec9e
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Wed Jul 11 11:14:51 2007 +0200
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Wed Jul 11 11:16:34 2007 +0200
     1.3 @@ -541,7 +541,7 @@
     1.4     below
     1.5  *)
     1.6  
     1.7 -inductive2
     1.8 +inductive
     1.9    members :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
    1.10      ("_ \<turnstile> _ member'_of _" [61,61,61] 60)
    1.11    for G :: prog
    1.12 @@ -634,7 +634,7 @@
    1.13  
    1.14  text {* Static overriding (used during the typecheck of the compiler) *}
    1.15  
    1.16 -inductive2
    1.17 +inductive
    1.18    stat_overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
    1.19      ("_ \<turnstile> _ overrides\<^sub>S _" [61,61,61] 60)
    1.20    for G :: prog
    1.21 @@ -653,7 +653,7 @@
    1.22  
    1.23  text {* Dynamic overriding (used during the typecheck of the compiler) *}
    1.24  
    1.25 -inductive2
    1.26 +inductive
    1.27    overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
    1.28      ("_ \<turnstile> _ overrides _" [61,61,61] 60)
    1.29    for G :: prog
    1.30 @@ -784,7 +784,7 @@
    1.31  \end{itemize} 
    1.32  *} 
    1.33  
    1.34 -inductive2
    1.35 +inductive
    1.36    accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
    1.37    and accessible_from :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
    1.38      ("_ \<turnstile> _ of _ accessible'_from _" [61,61,61,61] 60)
    1.39 @@ -828,7 +828,7 @@
    1.40  "G\<turnstile>Field fn f of C accessible_from accclass"  
    1.41   \<rightleftharpoons> "G\<turnstile>(fieldm fn f) of C accessible_from accclass" 
    1.42  
    1.43 -inductive2
    1.44 +inductive
    1.45    dyn_accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
    1.46    and dyn_accessible_from' ::  "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
    1.47      ("_ \<turnstile> _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)