src/HOL/Bali/DeclConcepts.thy
changeset 59682 d662d096f72b
parent 58887 38db8ddc0f57
child 61424 c3658c18b7bc
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Tue Mar 10 23:04:40 2015 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Thu Mar 12 14:58:32 2015 +0100
     1.3 @@ -368,7 +368,7 @@
     1.4  class) to a qualified member declaration:  @{text method}  *}
     1.5  
     1.6  definition
     1.7 -  method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
     1.8 +  "method" :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
     1.9    where "method sig m = (declclass m, mdecl (sig, mthd m))"
    1.10  
    1.11  lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"