11 text {* |
10 text {* |
12 This theory provides definitions for the @{text Object} class, |
11 This theory provides definitions for the @{text Object} class, |
13 and the system exceptions. |
12 and the system exceptions. |
14 *} |
13 *} |
15 |
14 |
16 constdefs |
15 definition ObjectC :: "'c cdecl" where |
17 ObjectC :: "'c cdecl" |
|
18 "ObjectC \<equiv> (Object, (undefined,[],[]))" |
16 "ObjectC \<equiv> (Object, (undefined,[],[]))" |
19 |
17 |
20 NullPointerC :: "'c cdecl" |
18 definition NullPointerC :: "'c cdecl" where |
21 "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))" |
19 "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))" |
22 |
20 |
23 ClassCastC :: "'c cdecl" |
21 definition ClassCastC :: "'c cdecl" where |
24 "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))" |
22 "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))" |
25 |
23 |
26 OutOfMemoryC :: "'c cdecl" |
24 definition OutOfMemoryC :: "'c cdecl" where |
27 "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))" |
25 "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))" |
28 |
26 |
29 SystemClasses :: "'c cdecl list" |
27 definition SystemClasses :: "'c cdecl list" where |
30 "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]" |
28 "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]" |
31 |
29 |
32 end |
30 end |