# HG changeset patch
# User haftmann
# Date 1285144224 -7200
# Node ID 23bdf736d84f83747693c7db0f5fec23643f55b3
# Parent  0af12dea761f261b33b73e4611e20904bdb9af27
tuned text

diff -r 0af12dea761f -r 23bdf736d84f src/HOL/Imperative_HOL/Overview.thy
--- a/src/HOL/Imperative_HOL/Overview.thy	Wed Sep 22 10:22:50 2010 +0200
+++ b/src/HOL/Imperative_HOL/Overview.thy	Wed Sep 22 10:30:24 2010 +0200
@@ -61,7 +61,7 @@
   fact collection @{text execute_simps} contains appropriate rewrites
   for all fundamental operations.
 
-  Primitive fine-granular control over heaps is avialable through rule
+  Primitive fine-granular control over heaps is available through rule
   @{text Heap_cases}:
 
   \begin{quote}
@@ -231,13 +231,13 @@
       
     \item Whether one should prefer equational reasoning (fact
       collection @{text execute_simps} or relational reasoning (fact
-      collections @{text crel_intros} and @{text crel_elims}) dependes
-      on the problems.  For complex expressions or expressions
-      involving binders, the relation style usually is superior but
-      requires more proof text.
+      collections @{text crel_intros} and @{text crel_elims}) depends
+      on the problems to solve.  For complex expressions or
+      expressions involving binders, the relation style usually is
+      superior but requires more proof text.
 
     \item Note that you can extend the fact collections of Imperative
-      HOL yourself.
+      HOL yourself whenever appropriate.
 
   \end{itemize}
 *}