isabelle: src/HOL/MicroJava/J/SystemClasses.thy@b7157c137855 (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
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	6	section \<open>System Classes\<close>
12951 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
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	10	text \<open>
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61361 diff changeset	11	This theory provides definitions for the \<open>Object\<close> class,
12951 a9fdcb71d252 introduces SystemClasses and BVExample kleing parents: diff changeset	12	and the system exceptions.
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	13	\<close>
12951 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
	Wed, 11 Oct 2023 14:03:16 +0200
changeset 78763	b7157c137855
parent 62042	6c6ccf573479
permissions	-rw-r--r--