equal
deleted
inserted
replaced
132 |
132 |
133 type_synonym oref = "loc + qtname" \<comment> \<open>generalized object reference\<close> |
133 type_synonym oref = "loc + qtname" \<comment> \<open>generalized object reference\<close> |
134 syntax |
134 syntax |
135 Heap :: "loc \<Rightarrow> oref" |
135 Heap :: "loc \<Rightarrow> oref" |
136 Stat :: "qtname \<Rightarrow> oref" |
136 Stat :: "qtname \<Rightarrow> oref" |
|
137 |
|
138 syntax_consts |
|
139 Heap == Inl and |
|
140 Stat == Inr |
137 |
141 |
138 translations |
142 translations |
139 "Heap" => "CONST Inl" |
143 "Heap" => "CONST Inl" |
140 "Stat" => "CONST Inr" |
144 "Stat" => "CONST Inr" |
141 (type) "oref" <= (type) "loc + qtname" |
145 (type) "oref" <= (type) "loc + qtname" |