# HG changeset patch
# User haftmann
# Date 1285578728 -7200
# Node ID e9bec0b43449da31cd0bfcbd2809cbe1b6112e2e
# Parent  d1c12f4ee9ac7968d687c00ba06c96ec1f47087f
added hint on reference equality

diff -r d1c12f4ee9ac -r e9bec0b43449 src/HOL/Imperative_HOL/Overview.thy
--- 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 *}