src/HOL/MicroJava/J/Value.thy
changeset 11701 3d51fbf81c17
parent 11070 cc421547e744
child 11908 82f68fd05094
equal deleted inserted replaced
11700:a0e6bda62b7b 11701:3d51fbf81c17
    38   default_val :: "ty => val"   (* default value for all types *)
    38   default_val :: "ty => val"   (* default value for all types *)
    39 
    39 
    40 primrec
    40 primrec
    41   "defpval Void    = Unit"
    41   "defpval Void    = Unit"
    42   "defpval Boolean = Bool False"
    42   "defpval Boolean = Bool False"
    43   "defpval Integer = Intg (#0)"
    43   "defpval Integer = Intg (Numeral0)"
    44 
    44 
    45 primrec
    45 primrec
    46   "default_val (PrimT pt) = defpval pt"
    46   "default_val (PrimT pt) = defpval pt"
    47   "default_val (RefT  r ) = Null"
    47   "default_val (RefT  r ) = Null"
    48 
    48