src/HOL/MicroJava/J/SystemClasses.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 16417 9bc16273c2d4
child 28524 644b62cf678f
permissions -rw-r--r--
Name.uu, Name.aT;
     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 imports Decl begin
    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