isabelle: src/HOL/MicroJava/J/SystemClasses.thy@322d1657c40c (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
44035 322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV Andreas Lochbihler parents: 35416 diff changeset	16	[code_inline]: "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
44035 322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV Andreas Lochbihler parents: 35416 diff changeset	19	[code_inline]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
12951 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
44035 322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV Andreas Lochbihler parents: 35416 diff changeset	22	[code_inline]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
12951 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
44035 322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV Andreas Lochbihler parents: 35416 diff changeset	25	[code_inline]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
12951 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
44035 322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV Andreas Lochbihler parents: 35416 diff changeset	28	[code_inline]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
12951 a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	29
a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	30	end

author	Andreas Lochbihler
	Fri, 05 Aug 2011 14:16:44 +0200
changeset 44035	322d1657c40c
parent 35416	d8d7d1b785af
child 45231	d85a2fdc586c
permissions	-rw-r--r--