| changeset 62042 | 6c6ccf573479 |
| parent 44890 | 22f665a2e91c |
| child 72990 | db8f94656024 |
--- a/src/HOL/Hoare/SepLogHeap.thy Sat Jan 02 18:46:36 2016 +0100 +++ b/src/HOL/Hoare/SepLogHeap.thy Sat Jan 02 18:48:45 2016 +0100 @@ -12,8 +12,8 @@ type_synonym heap = "(nat \<Rightarrow> nat option)" -text{* @{text "Some"} means allocated, @{text "None"} means -free. Address @{text "0"} serves as the null reference. *} +text\<open>\<open>Some\<close> means allocated, \<open>None\<close> means +free. Address \<open>0\<close> serves as the null reference.\<close> subsection "Paths in the heap"