# HG changeset patch
# User haftmann
# Date 1288874556 -3600
# Node ID b6ed3364753d737adaa09363dce8dc8ad184c2aa
# Parent  d7dfec07806a6c9ab919032515002e6ce28c285f
added note on countable types

diff -r d7dfec07806a -r b6ed3364753d src/HOL/Imperative_HOL/Overview.thy
--- a/src/HOL/Imperative_HOL/Overview.thy	Thu Nov 04 09:54:16 2010 +0100
+++ b/src/HOL/Imperative_HOL/Overview.thy	Thu Nov 04 13:42:36 2010 +0100
@@ -31,7 +31,7 @@
   realisation has changed since, due to both extensions and
   refinements.  Therefore this overview wants to present the framework
   \qt{as it is} by now.  It focusses on the user-view, less on matters
-  of constructions.  For details study of the theory sources is
+  of construction.  For details study of the theory sources is
   encouraged.
 *}
 
@@ -41,7 +41,8 @@
 text {*
   Heaps (@{type heap}) can be populated by values of class @{class
   heap}; HOL's default types are already instantiated to class @{class
-  heap}.
+  heap}.  Class @{class heap} is a subclass of @{class countable};  see
+  theory @{text Countable} for ways to instantiate types as @{class countable}.
 
   The heap is wrapped up in a monad @{typ "'a Heap"} by means of the
   following specification:
@@ -100,7 +101,7 @@
 
   provides a simple relational calculus.  Primitive rules are @{text
   crelI} and @{text crelE}, rules appropriate for reasoning about
-  imperative operation are available in the @{text crel_intros} and
+  imperative operations are available in the @{text crel_intros} and
   @{text crel_elims} fact collections.
 
   Often non-failure of imperative computations does not depend