isabelle: src/HOL/MicroJava/J/SystemClasses.thy@42804fb5dd92 (annotated)

12951 a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	1	(* Title: HOL/MicroJava/J/SystemClasses.thy
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	2	Author: Gerwin Klein
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	3	Copyright 2002 Technische Universitaet Muenchen
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	4	*)
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	5
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	6	header {* \isaheader{System Classes} *}
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	7
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 12951 diff changeset	8	theory SystemClasses imports Decl begin
12951 a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	9
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	10	text {*
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	11	This theory provides definitions for the @{text Object} class,
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	12	and the system exceptions.
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	13	*}
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	14
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 28524 diff changeset	15	definition ObjectC :: "'c cdecl" where
28524 644b62cf678f arbitrary is undefined haftmann parents: 16417 diff changeset	16	"ObjectC \<equiv> (Object, (undefined,[],[]))"
12951 a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	17
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 28524 diff changeset	18	definition NullPointerC :: "'c cdecl" where
12951 a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	19	"NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	20
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 28524 diff changeset	21	definition ClassCastC :: "'c cdecl" where
12951 a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	22	"ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	23
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 28524 diff changeset	24	definition OutOfMemoryC :: "'c cdecl" where
12951 a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	25	"OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	26
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 28524 diff changeset	27	definition SystemClasses :: "'c cdecl list" where
12951 a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	28	"SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	29
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	30	end

author	wenzelm
	Thu, 24 Jun 2010 14:31:01 +0200
changeset 37528	42804fb5dd92
parent 35416	d8d7d1b785af
child 44035	322d1657c40c
permissions	-rw-r--r--