fixed two typos in IMP (by Jean Pichon)
authorkleing
Wed Sep 21 09:17:01 2011 +1000 (2011-09-21)
changeset 4501707a0638c351a
parent 45016 a5d43ffc95eb
child 45018 020e460b6644
fixed two typos in IMP (by Jean Pichon)
src/HOL/IMP/AbsInt1.thy
src/HOL/IMP/AbsInt2.thy
     1.1 --- a/src/HOL/IMP/AbsInt1.thy	Wed Sep 21 00:12:36 2011 +0200
     1.2 +++ b/src/HOL/IMP/AbsInt1.thy	Wed Sep 21 09:17:01 2011 +1000
     1.3 @@ -122,7 +122,7 @@
     1.4  
     1.5  text{* The test for @{const Bot} in the @{const V}-case is important: @{const
     1.6  Bot} indicates that a variable has no possible values, i.e.\ that the current
     1.7 -program point is unreachable. But then the abstract state should collaps to
     1.8 +program point is unreachable. But then the abstract state should collapse to
     1.9  @{const bot}. Put differently, we maintain the invariant that in an abstract
    1.10  state all variables are mapped to non-@{const Bot} values. Otherwise the
    1.11  (pointwise) join of two abstract states, one of which contains @{const Bot}
     2.1 --- a/src/HOL/IMP/AbsInt2.thy	Wed Sep 21 00:12:36 2011 +0200
     2.2 +++ b/src/HOL/IMP/AbsInt2.thy	Wed Sep 21 09:17:01 2011 +1000
     2.3 @@ -6,7 +6,7 @@
     2.4  
     2.5  subsection "Widening and Narrowing"
     2.6  
     2.7 -text{* The assumptions about winden and narrow are merely sanity checks. They
     2.8 +text{* The assumptions about widen and narrow are merely sanity checks. They
     2.9  are only needed in case we want to prove termination of the fixedpoint
    2.10  iteration, which we do not --- we limit the number of iterations as before. *}
    2.11