author | huffman |
Mon, 26 Apr 2010 10:57:04 -0700 | |
changeset 36366 | 886b94b1bed7 |
parent 36365 | 18bf20d0c2df |
child 36367 | 49c7dee21a7f |
--- a/src/HOL/Bali/DeclConcepts.thy Mon Apr 26 09:45:22 2010 -0700 +++ b/src/HOL/Bali/DeclConcepts.thy Mon Apr 26 10:57:04 2010 -0700 @@ -1390,7 +1390,7 @@ "accimethds G pack I \<equiv> if G\<turnstile>Iface I accessible_in pack then imethds G I - else \<lambda> k. {}" + else (\<lambda> k. {})" text {* only returns imethds if the interface is accessible *} definition methd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where