added hint on reference equality

--- a/src/HOL/Imperative_HOL/Overview.thy	Mon Sep 27 11:12:01 2010 +0200
+++ b/src/HOL/Imperative_HOL/Overview.thy	Mon Sep 27 11:12:08 2010 +0200
@@ -138,6 +138,9 @@
 
   Provided proof rules are such that they reduce monad operations to
   operations on bare heaps.
+
+  Note that HOL equality coincides with reference equality and may be
+  used as primitive executable operation.
 *}
 
 subsection {* Arrays *}