(* Title: Jinja/J/State.thy
Author: Tobias Nipkow
Copyright 2003 Technische Universitaet Muenchen
*)
section ‹Program State›
theory State imports "../Common/Exceptions" begin
type_synonym
locals = "vname ⇀ val" ― ‹local vars, incl. params and ``this''›
type_synonym
state = "heap × locals"
definition hp :: "state → heap"
where
"hp ≡ fst"
definition lcl :: "state → locals"
where
"lcl ≡ snd"
(*<*)
declare hp_def[simp] lcl_def[simp]
(*>*)
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet am 2026-11-04)
¤
*© Formatika GbR, Deutschland