equal
deleted
inserted
replaced
8 |
8 |
9 theory SepLogHeap |
9 theory SepLogHeap |
10 imports Main |
10 imports Main |
11 begin |
11 begin |
12 |
12 |
13 types heap = "(nat \<Rightarrow> nat option)" |
13 type_synonym heap = "(nat \<Rightarrow> nat option)" |
14 |
14 |
15 text{* @{text "Some"} means allocated, @{text "None"} means |
15 text{* @{text "Some"} means allocated, @{text "None"} means |
16 free. Address @{text "0"} serves as the null reference. *} |
16 free. Address @{text "0"} serves as the null reference. *} |
17 |
17 |
18 subsection "Paths in the heap" |
18 subsection "Paths in the heap" |