# HG changeset patch
# User haftmann
# Date 1278400873 -7200
# Node ID 831b3eb7ed8e7cb0c4c47a1e8fe645e2d4e95a2b
# Parent  2d232a1f39c275057c15e8a85a172b6fcbfc89ea
tuned empty heap

diff -r 2d232a1f39c2 -r 831b3eb7ed8e src/HOL/Imperative_HOL/Heap.thy
--- 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