src/HOL/MicroJava/J/SystemClasses.thy
changeset 61361 8b5f00202e1a
parent 58886 8a6cac7c7247
child 62042 6c6ccf573479
equal deleted inserted replaced
61360:a273bdac0934 61361:8b5f00202e1a
     1 (*  Title:      HOL/MicroJava/J/SystemClasses.thy
     1 (*  Title:      HOL/MicroJava/J/SystemClasses.thy
     2     Author:     Gerwin Klein
     2     Author:     Gerwin Klein
     3     Copyright   2002 Technische Universitaet Muenchen
     3     Copyright   2002 Technische Universitaet Muenchen
     4 *)
     4 *)
     5 
     5 
     6 section {* System Classes *}
     6 section \<open>System Classes\<close>
     7 
     7 
     8 theory SystemClasses imports Decl begin
     8 theory SystemClasses imports Decl begin
     9 
     9 
    10 text {*
    10 text \<open>
    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 \<close>
    14 
    14 
    15 definition ObjectC :: "'c cdecl" where
    15 definition ObjectC :: "'c cdecl" where
    16   [code_unfold]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
    16   [code_unfold]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
    17 
    17 
    18 definition NullPointerC :: "'c cdecl" where
    18 definition NullPointerC :: "'c cdecl" where