src/HOL/Bali/DeclConcepts.thy

                                  ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60)
 
 "G\<turnstile>m undeclared_in C \<equiv> (case m of
                             fid fn  \<Rightarrow> cdeclaredfield G C fn  = None
                           | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
-
-lemma method_declared_inI:
-  "\<lbrakk>class G C = Some c; table_of (methods c) sig = Some m\<rbrakk> 
-   \<Longrightarrow> G\<turnstile>mdecl (sig,m) declared_in C"
-by (auto simp add: declared_in_def cdeclaredmethd_def)
 
 
 subsubsection "members"
 
 consts