src/HOL/MicroJava/J/SystemClasses.thy
changeset 44035 322d1657c40c
parent 35416 d8d7d1b785af
child 45231 d85a2fdc586c
equal deleted inserted replaced
44034:53a081c8873d 44035:322d1657c40c
    11   This theory provides definitions for the @{text Object} class,
    11   This theory provides definitions for the @{text Object} class,
    12   and the system exceptions.
    12   and the system exceptions.
    13 *}
    13 *}
    14 
    14 
    15 definition ObjectC :: "'c cdecl" where
    15 definition ObjectC :: "'c cdecl" where
    16   "ObjectC \<equiv> (Object, (undefined,[],[]))"
    16   [code_inline]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
    17 
    17 
    18 definition NullPointerC :: "'c cdecl" where
    18 definition NullPointerC :: "'c cdecl" where
    19   "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
    19   [code_inline]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
    20 
    20 
    21 definition ClassCastC :: "'c cdecl" where
    21 definition ClassCastC :: "'c cdecl" where
    22   "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
    22   [code_inline]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
    23 
    23 
    24 definition OutOfMemoryC :: "'c cdecl" where
    24 definition OutOfMemoryC :: "'c cdecl" where
    25   "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
    25   [code_inline]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
    26 
    26 
    27 definition SystemClasses :: "'c cdecl list" where
    27 definition SystemClasses :: "'c cdecl list" where
    28   "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
    28   [code_inline]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
    29 
    29 
    30 end
    30 end