src/HOL/MicroJava/J/Decl.thy
changeset 12951 a9fdcb71d252
parent 12911 704713ca07ea
child 14134 0fdf5708c7a8
--- a/src/HOL/MicroJava/J/Decl.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -23,11 +23,6 @@
   'c prog  = "'c cdecl list"     -- "program"
 
 
-constdefs
-  ObjectC :: "'c cdecl" -- "decl of root class"
-  "ObjectC \<equiv> (Object, (arbitrary, [], []))"
-
-
 translations
   "fdecl"   <= (type) "vname \<times> ty"
   "sig"     <= (type) "mname \<times> ty list"