Theory State

(*  Title:      Jinja/J/State.thy
    ID:         $Id: State.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

header {* \isaheader{Program State} *}

theory State = Exceptions:

types
  locals = "vname => val"      -- "local vars, incl. params and ``this''"
  state  = "heap × locals"

constdefs
  hp :: "state => heap"
  "hp  ≡  fst"
  lcl :: "state => locals"
  "lcl  ≡  snd"

(*<*)
declare hp_def[simp] lcl_def[simp]
(*>*)
end