Theory SystemClasses

Up to index of Isabelle/HOL/CoreC++

theory SystemClasses
imports Exceptions

(*  Title:       CoreC++
    ID:          $Id: SystemClasses.thy,v 1.6 2006-11-06 11:54:13 wasserra Exp $
    Author:      Gerwin Klein
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
*)

header {* \isaheader{System Classes} *}

theory SystemClasses imports Exceptions begin


text {*
  This theory provides definitions for the system exceptions.
*}

constdefs
  NullPointerC :: "cdecl"
  "NullPointerC ≡ (NullPointer, ([],[],[]))"

  ClassCastC :: "cdecl"
  "ClassCastC ≡ (ClassCast, ([],[],[]))"

  OutOfMemoryC :: "cdecl"
  "OutOfMemoryC ≡ (OutOfMemory, ([],[],[]))"

  SystemClasses :: "cdecl list"
  "SystemClasses ≡ [NullPointerC, ClassCastC, OutOfMemoryC]"

end