author | haftmann |

Thu Nov 04 13:42:36 2010 +0100 (2010-11-04) | |

changeset 40358 | b6ed3364753d |

parent 40354 | d7dfec07806a |

child 40359 | 84388bba911d |

added note on countable types

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