src/HOL/MicroJava/J/State.thy
changeset 12911 704713ca07ea
parent 12545 7319d384d0d3
child 13672 b95d12325b51
equal deleted inserted replaced
12910:f5bceeec9d91 12911:704713ca07ea
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     David von Oheimb
     3     Author:     David von Oheimb
     4     Copyright   1999 Technische Universitaet Muenchen
     4     Copyright   1999 Technische Universitaet Muenchen
     5 *)
     5 *)
     6 
     6 
     7 header "Program State"
     7 header {* \isaheader{Program State} *}
     8 
     8 
     9 theory State = TypeRel + Value:
     9 theory State = TypeRel + Value:
    10 
    10 
    11 types 
    11 types 
    12   fields_ = "(vname \<times> cname \<leadsto> val)"  -- "field name, defining class, value"
    12   fields_ = "(vname \<times> cname \<leadsto> val)"  -- "field name, defining class, value"