equal
deleted
inserted
replaced
8 imports Array |
8 imports Array |
9 begin |
9 begin |
10 |
10 |
11 text \<open> |
11 text \<open> |
12 Imperative reference operations; modeled after their ML counterparts. |
12 Imperative reference operations; modeled after their ML counterparts. |
13 See @{url "http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html"} |
13 See \<^url>\<open>http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html\<close> |
14 and @{url "http://www.smlnj.org/doc/Conversion/top-level-comparison.html"} |
14 and \<^url>\<open>http://www.smlnj.org/doc/Conversion/top-level-comparison.html\<close>. |
15 \<close> |
15 \<close> |
16 |
16 |
17 subsection \<open>Primitives\<close> |
17 subsection \<open>Primitives\<close> |
18 |
18 |
19 definition present :: "heap \<Rightarrow> 'a::heap ref \<Rightarrow> bool" where |
19 definition present :: "heap \<Rightarrow> 'a::heap ref \<Rightarrow> bool" where |