Theory SystemClasses
section ‹System Classes›
theory SystemClasses imports Exceptions begin
text ‹
This theory provides definitions for the system exceptions.
›
definition NullPointerC :: "cdecl" where
"NullPointerC ≡ (NullPointer, ([],[],[]))"
definition ClassCastC :: "cdecl" where
"ClassCastC ≡ (ClassCast, ([],[],[]))"
definition OutOfMemoryC :: "cdecl" where
"OutOfMemoryC ≡ (OutOfMemory, ([],[],[]))"
definition SystemClasses :: "cdecl list" where
"SystemClasses ≡ [NullPointerC, ClassCastC, OutOfMemoryC]"
end