author | paulson <lp15@cam.ac.uk> |
Wed, 24 Apr 2024 09:21:44 +0100 | |
changeset 80148 | b156869b826a |
parent 62042 | 6c6ccf573479 |
permissions | -rw-r--r-- |
12951 | 1 |
(* Title: HOL/MicroJava/J/SystemClasses.thy |
2 |
Author: Gerwin Klein |
|
3 |
Copyright 2002 Technische Universitaet Muenchen |
|
4 |
*) |
|
5 |
||
61361 | 6 |
section \<open>System Classes\<close> |
12951 | 7 |
|
16417 | 8 |
theory SystemClasses imports Decl begin |
12951 | 9 |
|
61361 | 10 |
text \<open> |
62042 | 11 |
This theory provides definitions for the \<open>Object\<close> class, |
12951 | 12 |
and the system exceptions. |
61361 | 13 |
\<close> |
12951 | 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 | 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 | 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 | 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 | 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 | 29 |
|
30 |
end |