equal
deleted
inserted
replaced
|
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 |
|
9 theory SystemClasses = Decl: |
|
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 |