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"