author | wenzelm |
Sat, 07 Apr 2012 16:41:59 +0200 | |
changeset 47389 | e8552cba702d |
parent 45231 | d85a2fdc586c |
child 58886 | 8a6cac7c7247 |
permissions | -rw-r--r-- |
12951 | 1 |
(* Title: HOL/MicroJava/J/SystemClasses.thy |
2 |
Author: Gerwin Klein |
|
3 |
Copyright 2002 Technische Universitaet Muenchen |
|
4 |
*) |
|
5 |
||
6 |
header {* \isaheader{System Classes} *} |
|
7 |
||
16417 | 8 |
theory SystemClasses imports Decl begin |
12951 | 9 |
|
10 |
text {* |
|
11 |
This theory provides definitions for the @{text Object} class, |
|
12 |
and the system exceptions. |
|
13 |
*} |
|
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 |