|
12951
|
1 |
(* Title: HOL/MicroJava/J/SystemClasses.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Gerwin Klein
|
|
|
4 |
Copyright 2002 Technische Universitaet Muenchen
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
header {* \isaheader{System Classes} *}
|
|
|
8 |
|
|
16417
|
9 |
theory SystemClasses imports Decl begin
|
|
12951
|
10 |
|
|
|
11 |
text {*
|
|
|
12 |
This theory provides definitions for the @{text Object} class,
|
|
|
13 |
and the system exceptions.
|
|
|
14 |
*}
|
|
|
15 |
|
|
|
16 |
constdefs
|
|
|
17 |
ObjectC :: "'c cdecl"
|
|
|
18 |
"ObjectC \<equiv> (Object, (arbitrary,[],[]))"
|
|
|
19 |
|
|
|
20 |
NullPointerC :: "'c cdecl"
|
|
|
21 |
"NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
|
|
|
22 |
|
|
|
23 |
ClassCastC :: "'c cdecl"
|
|
|
24 |
"ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
|
|
|
25 |
|
|
|
26 |
OutOfMemoryC :: "'c cdecl"
|
|
|
27 |
"OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
|
|
|
28 |
|
|
|
29 |
SystemClasses :: "'c cdecl list"
|
|
|
30 |
"SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
|
|
|
31 |
|
|
|
32 |
end
|