src/HOL/Bali/Value.thy
changeset 17160 fb65eda72fc7
parent 16417 9bc16273c2d4
child 32960 69916a850301
equal deleted inserted replaced
17159:d5060118122e 17160:fb65eda72fc7
     7 
     7 
     8 
     8 
     9 theory Value imports Type begin
     9 theory Value imports Type begin
    10 
    10 
    11 typedecl loc            --{* locations, i.e. abstract references on objects *}
    11 typedecl loc            --{* locations, i.e. abstract references on objects *}
    12 arities	 loc :: "type"
       
    13 
    12 
    14 datatype val
    13 datatype val
    15 	= Unit          --{* dummy result value of void methods *}
    14 	= Unit          --{* dummy result value of void methods *}
    16 	| Bool bool     --{* Boolean value *}
    15 	| Bool bool     --{* Boolean value *}
    17 	| Intg int      --{* integer value *}
    16 	| Intg int      --{* integer value *}