equal
deleted
inserted
replaced
40 text {* |
40 text {* |
41 References and arrays are developed in parallel, |
41 References and arrays are developed in parallel, |
42 but keeping them separate makes some later proofs simpler. |
42 but keeping them separate makes some later proofs simpler. |
43 *} |
43 *} |
44 |
44 |
45 types addr = nat -- "untyped heap references" |
45 type_synonym addr = nat -- "untyped heap references" |
46 types heap_rep = nat -- "representable values" |
46 type_synonym heap_rep = nat -- "representable values" |
47 |
47 |
48 record heap = |
48 record heap = |
49 arrays :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep list" |
49 arrays :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep list" |
50 refs :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep" |
50 refs :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep" |
51 lim :: addr |
51 lim :: addr |