1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/MicroJava/J/Decl.thy	Thu Nov 11 12:23:45 1999 +0100
     1.3 @@ -0,0 +1,37 @@
     1.4 +(*  Title:      HOL/MicroJava/J/Decl.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb
     1.7 +    Copyright   1997 Technische Universitaet Muenchen
     1.8 +
     1.9 +Class declarations
    1.10 +*)
    1.11 +
    1.12 +Decl = Type +
    1.13 +
    1.14 +types	fdecl		(* field declaration, cf. 8.3 (, 9.3) *)
    1.15 +	= "vname \\<times> ty"
    1.16 +
    1.17 +
    1.18 +types	sig		(* signature of a method, cf. 8.4.2 *)
    1.19 +	= "mname \\<times> ty list"
    1.20 +
    1.21 +	'c mdecl		(* method declaration in a class *)
    1.22 +	= "sig \\<times> ty \\<times> 'c"
    1.23 +
    1.24 +types	'c class		(* class *)
    1.25 +	= "cname option \\<times> fdecl list \\<times> 'c mdecl list"
    1.26 +	(* superclass, fields, methods*)
    1.27 +
    1.28 +	'c cdecl		(* class declaration, cf. 8.1 *)
    1.29 +	= "cname \\<times> 'c class"
    1.30 +
    1.31 +consts
    1.32 +
    1.33 +  Object  :: cname	(* name of root class *)
    1.34 +  ObjectC :: 'c cdecl	(* decl of root class *)
    1.35 +
    1.36 +defs 
    1.37 +
    1.38 + ObjectC_def "ObjectC \\<equiv> (Object, (None, [], []))"
    1.39 +
    1.40 +end