--- a/src/HOL/NanoJava/Decl.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/NanoJava/Decl.thy Mon Mar 01 13:40:23 2010 +0100
@@ -50,11 +50,10 @@
Object :: cname --{* name of root class *}
-constdefs
- "class" :: "cname \<rightharpoonup> class"
+definition "class" :: "cname \<rightharpoonup> class" where
"class \<equiv> map_of Prog"
- is_class :: "cname => bool"
+definition is_class :: "cname => bool" where
"is_class C \<equiv> class C \<noteq> None"
lemma finite_is_class: "finite {C. is_class C}"