--- a/src/HOL/Bali/Example.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/Bali/Example.thy Mon Jan 11 21:21:02 2016 +0100
@@ -141,12 +141,16 @@
lemma neq_Main_SXcpt [simp]: "Main\<noteq>SXcpt xn"
by (simp add: SXcpt_def)
+
subsubsection "classes and interfaces"
-defs
-
- Object_mdecls_def: "Object_mdecls \<equiv> []"
- SXcpt_mdecls_def: "SXcpt_mdecls \<equiv> []"
+overloading
+ Object_mdecls \<equiv> Object_mdecls
+ SXcpt_mdecls \<equiv> SXcpt_mdecls
+begin
+ definition "Object_mdecls \<equiv> []"
+ definition "SXcpt_mdecls \<equiv> []"
+end
axiomatization
foo :: mname