isabelle: src/HOL/MicroJava/J/SystemClasses.thy@61ac1efe02c3 (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
45231 d85a2fdc586c replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed bulwahn parents: 44035 diff changeset	16	[code_unfold]: "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
45231 d85a2fdc586c replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed bulwahn parents: 44035 diff changeset	19	[code_unfold]: "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
45231 d85a2fdc586c replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed bulwahn parents: 44035 diff changeset	22	[code_unfold]: "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
45231 d85a2fdc586c replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed bulwahn parents: 44035 diff changeset	25	[code_unfold]: "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
45231 d85a2fdc586c replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed bulwahn parents: 44035 diff changeset	28	[code_unfold]: "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	wenzelm
	Mon, 13 May 2013 13:23:13 +0200
changeset 51960	61ac1efe02c3
parent 45231	d85a2fdc586c
child 58886	8a6cac7c7247
permissions	-rw-r--r--