changeset 12338 | de0f4a63baa5 |
parent 11070 | cc421547e744 |
child 12517 | 360e3215f029 |
--- a/src/HOL/MicroJava/J/Type.thy Sat Dec 01 18:51:46 2001 +0100 +++ b/src/HOL/MicroJava/J/Type.thy Sat Dec 01 18:52:32 2001 +0100 @@ -11,9 +11,6 @@ typedecl cname (* class name *) typedecl vnam (* variable or field name *) typedecl mname (* method name *) -arities cname :: "term" - vnam :: "term" - mname :: "term" datatype vname (* names for This pointer and local/field variables *) = This