added note on countable types
authorhaftmann
Thu Nov 04 13:42:36 2010 +0100 (2010-11-04)
changeset 40358b6ed3364753d
parent 40354 d7dfec07806a
child 40359 84388bba911d
added note on countable types
src/HOL/Imperative_HOL/Overview.thy
     1.1 --- a/src/HOL/Imperative_HOL/Overview.thy	Thu Nov 04 09:54:16 2010 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Overview.thy	Thu Nov 04 13:42:36 2010 +0100
     1.3 @@ -31,7 +31,7 @@
     1.4    realisation has changed since, due to both extensions and
     1.5    refinements.  Therefore this overview wants to present the framework
     1.6    \qt{as it is} by now.  It focusses on the user-view, less on matters
     1.7 -  of constructions.  For details study of the theory sources is
     1.8 +  of construction.  For details study of the theory sources is
     1.9    encouraged.
    1.10  *}
    1.11  
    1.12 @@ -41,7 +41,8 @@
    1.13  text {*
    1.14    Heaps (@{type heap}) can be populated by values of class @{class
    1.15    heap}; HOL's default types are already instantiated to class @{class
    1.16 -  heap}.
    1.17 +  heap}.  Class @{class heap} is a subclass of @{class countable};  see
    1.18 +  theory @{text Countable} for ways to instantiate types as @{class countable}.
    1.19  
    1.20    The heap is wrapped up in a monad @{typ "'a Heap"} by means of the
    1.21    following specification:
    1.22 @@ -100,7 +101,7 @@
    1.23  
    1.24    provides a simple relational calculus.  Primitive rules are @{text
    1.25    crelI} and @{text crelE}, rules appropriate for reasoning about
    1.26 -  imperative operation are available in the @{text crel_intros} and
    1.27 +  imperative operations are available in the @{text crel_intros} and
    1.28    @{text crel_elims} fact collections.
    1.29  
    1.30    Often non-failure of imperative computations does not depend