Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/J/Decl.thy
author paulson
Wed, 21 Jun 2000 10:31:34 +0200
changeset 9097 44cd0f9f8e5b
parent 8011 d14c4e9e9c8e
child 9346 297dcbf64526
permissions -rw-r--r--
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split

(*  Title:      HOL/MicroJava/J/Decl.thy
    ID:         $Id$
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen

Class declarations
*)

Decl = Type +

types	fdecl		(* field declaration, cf. 8.3 (, 9.3) *)
	= "vname \\<times> ty"


types	sig		(* signature of a method, cf. 8.4.2 *)
	= "mname \\<times> ty list"

	'c mdecl		(* method declaration in a class *)
	= "sig \\<times> ty \\<times> 'c"

types	'c class		(* class *)
	= "cname option \\<times> fdecl list \\<times> 'c mdecl list"
	(* superclass, fields, methods*)

	'c cdecl		(* class declaration, cf. 8.1 *)
	= "cname \\<times> 'c class"

consts

  Object  :: cname	(* name of root class *)
  ObjectC :: 'c cdecl	(* decl of root class *)

defs 

 ObjectC_def "ObjectC \\<equiv> (Object, (None, [], []))"

end
isabelle