equal
deleted
inserted
replaced
366 |
366 |
367 text {* Convert a qualified method (qualified with its declaring |
367 text {* Convert a qualified method (qualified with its declaring |
368 class) to a qualified member declaration: @{text method} *} |
368 class) to a qualified member declaration: @{text method} *} |
369 |
369 |
370 definition |
370 definition |
371 method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)" |
371 "method" :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)" |
372 where "method sig m = (declclass m, mdecl (sig, mthd m))" |
372 where "method sig m = (declclass m, mdecl (sig, mthd m))" |
373 |
373 |
374 lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))" |
374 lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))" |
375 by (simp add: method_def) |
375 by (simp add: method_def) |
376 |
376 |