| changeset 42174 | d0be2722ce9f |
| parent 41959 | b460124855b8 |
| child 44890 | 22f665a2e91c |
--- a/src/HOL/Hoare/SepLogHeap.thy Wed Mar 30 22:53:18 2011 +0200 +++ b/src/HOL/Hoare/SepLogHeap.thy Wed Mar 30 23:26:40 2011 +0200 @@ -10,7 +10,7 @@ imports Main begin -types heap = "(nat \<Rightarrow> nat option)" +type_synonym heap = "(nat \<Rightarrow> nat option)" text{* @{text "Some"} means allocated, @{text "None"} means free. Address @{text "0"} serves as the null reference. *}