Isabelle2018: CamkesGlueSpec
This commit is contained in:
parent
082a48d7b2
commit
b148b0c94a
|
@ -91,7 +91,7 @@ text {*
|
|||
definition
|
||||
init_memory_state :: "'component_state local_state"
|
||||
where
|
||||
"init_memory_state \<equiv> Memory empty"
|
||||
"init_memory_state \<equiv> Memory Map.empty"
|
||||
|
||||
text {*
|
||||
In \camkes ADL descriptions, shared memory regions can have a type, typically
|
||||
|
|
|
@ -109,7 +109,7 @@ type_synonym lstate = "component_state local_state"
|
|||
definition
|
||||
trusted :: "('inst, ('channel component \<times> lstate)) map"
|
||||
where
|
||||
"trusted \<equiv> empty"
|
||||
"trusted \<equiv> Map.empty"
|
||||
|
||||
(*<*)
|
||||
end
|
||||
|
|
Loading…
Reference in New Issue