--- a/src/HOL/Imperative_HOL/Heap.thy Mon Jul 05 16:43:08 2010 +0100
+++ b/src/HOL/Imperative_HOL/Heap.thy Tue Jul 06 09:21:13 2010 +0200
@@ -51,7 +51,7 @@
lim :: addr
definition empty :: heap where
- "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>" -- "why undefined?"
+ "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>"
datatype 'a array = Array addr
datatype 'a ref = Ref addr -- "note the phantom type 'a "
@@ -85,4 +85,6 @@
#> Sign.add_const_constraint (@{const_name addr_of_ref}, SOME @{typ "'a\<Colon>heap ref \<Rightarrow> nat"})
*}
+hide_const (open) empty
+
end