isabelle: src/HOL/MicroJava/J/Type.thy@c7226e6f9625 (annotated)

8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	1	(* Title: HOL/MicroJava/J/Type.thy
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	2	ID: $Id$
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	3	Author: David von Oheimb
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	4	Copyright 1999 Technische Universitaet Muenchen
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	5
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	6	Java types
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	7	*)
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	8
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	9	Type = JBasis +
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	10
10061 fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	11	types cname (* class name *)
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	12	vnam (* variable or field name *)
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	13	mname (* method name *)
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	14
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	15	arities cname, vnam, mname :: term
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	16
10069 c7226e6f9625 untabified for HTML kleing parents: 10061 diff changeset	17	datatype vname (* names for This pointer and local/field variables *)
10061 fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	18	= This
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	19	\| VName vnam
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	20
10061 fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	21	datatype prim_ty (* primitive type, cf. 4.2 *)
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	22	= Void (* 'result type' of void methods *)
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	23	\| Boolean
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	24	\| Integer
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	25
10069 c7226e6f9625 untabified for HTML kleing parents: 10061 diff changeset	26	datatype ref_ty (* reference type, cf. 4.3 *)
c7226e6f9625 untabified for HTML kleing parents: 10061 diff changeset	27	= NullT (* null type, cf. 4.1 *)
10061 fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	28	\| ClassT cname (* class type *)
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	29
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	30	datatype ty (* any type, cf. 4.1 *)
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	31	= PrimT prim_ty (* primitive type *)
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	32	\| RefT ref_ty (* reference type *)
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	33
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	34	syntax
10061 fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	35	NT :: " ty"
10069 c7226e6f9625 untabified for HTML kleing parents: 10061 diff changeset	36	Class :: "cname => ty"
10061 fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	37
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	38	translations
10069 c7226e6f9625 untabified for HTML kleing parents: 10061 diff changeset	39	"NT" == "RefT NullT"
c7226e6f9625 untabified for HTML kleing parents: 10061 diff changeset	40	"Class C" == "RefT (ClassT C)"
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	41
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	42	end

author	kleing
	Mon, 25 Sep 2000 12:08:49 +0200
changeset 10069	c7226e6f9625
parent 10061	fe82134773dc
child 11026	a50365d21144
permissions	-rw-r--r--