isabelle: src/HOL/MicroJava/J/Type.thy@cc7a0b9f938c (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	Author: David von Oheimb
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	3	Copyright 1999 Technische Universitaet Muenchen
11070 cc421547e744 improved document (added headers etc) oheimb parents: 11026 diff changeset	4	*)
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	5
12911 704713ca07ea new document kleing parents: 12517 diff changeset	6	header {* \isaheader{Java types} *}
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	7
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 12951 diff changeset	8	theory Type imports JBasis begin
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	9
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	10	typedecl cnam
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	11
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	12	-- "exceptions"
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	13	datatype
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	14	xcpt
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	15	= NullPointer
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	16	\| ClassCast
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	17	\| OutOfMemory
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	18
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	19	-- "class names"
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	20	datatype cname
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	21	= Object
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	22	\| Xcpt xcpt
12951 a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: 12911 diff changeset	23	\| Cname cnam
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	24
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	25	typedecl vnam -- "variable or field name"
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	26	typedecl mname -- "method name"
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	27
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	28	-- "names for @{text This} pointer and local/field variables"
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	29	datatype vname
10061 fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	30	= This
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	31	\| VName vnam
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	32
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	33	-- "primitive type, cf. 4.2"
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	34	datatype prim_ty
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	35	= Void -- "'result type' of void methods"
10061 fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	36	\| Boolean
fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	37	\| Integer
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	38
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	39	-- "reference type, cf. 4.3"
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	40	datatype ref_ty
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	41	= NullT -- "null type, cf. 4.1"
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	42	\| ClassT cname -- "class type"
10061 fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	43
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	44	-- "any type, cf. 4.1"
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	45	datatype ty
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	46	= PrimT prim_ty -- "primitive type"
360e3215f029 exception merge, cleanup, tuned kleing parents: 12338 diff changeset	47	\| RefT ref_ty -- "reference type"
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	48
35102 cc7a0b9f938c modernized translations; wenzelm parents: 16417 diff changeset	49	abbreviation NT :: ty
cc7a0b9f938c modernized translations; wenzelm parents: 16417 diff changeset	50	where "NT == RefT NullT"
10061 fe82134773dc added HTML syntax; added spaces in normal syntax for better documents kleing parents: 10042 diff changeset	51
35102 cc7a0b9f938c modernized translations; wenzelm parents: 16417 diff changeset	52	abbreviation Class :: "cname => ty"
cc7a0b9f938c modernized translations; wenzelm parents: 16417 diff changeset	53	where "Class C == RefT (ClassT C)"
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	54
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	55	end

author	wenzelm
	Thu, 11 Feb 2010 00:45:02 +0100
changeset 35102	cc7a0b9f938c
parent 16417	9bc16273c2d4
child 44035	322d1657c40c
permissions	-rwxr-xr-x