src/HOL/MicroJava/J/SystemClasses.thy
changeset 35416 d8d7d1b785af
parent 28524 644b62cf678f
child 44035 322d1657c40c
equal deleted inserted replaced
35342:4dc65845eab3 35416:d8d7d1b785af
     1 (*  Title:      HOL/MicroJava/J/SystemClasses.thy
     1 (*  Title:      HOL/MicroJava/J/SystemClasses.thy
     2     ID:         $Id$
       
     3     Author:     Gerwin Klein
     2     Author:     Gerwin Klein
     4     Copyright   2002 Technische Universitaet Muenchen
     3     Copyright   2002 Technische Universitaet Muenchen
     5 *)
     4 *)
     6 
     5 
     7 header {* \isaheader{System Classes} *}
     6 header {* \isaheader{System Classes} *}
    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