# HG changeset patch
# User nipkow
# Date 1675070101 -3600
# Node ID 5bf9a1b78f932b80afff45567bf90295ff7ec537
# Parent  515b6aaede327fca57f4a80bfb74da4333fd860c
text correction

diff -r 515b6aaede32 -r 5bf9a1b78f93 src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Sun Jan 29 16:49:17 2023 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Mon Jan 30 10:15:01 2023 +0100
@@ -432,7 +432,7 @@
 text\<open>Takes as many iterations as the actual execution. Would diverge if
 loop did not terminate. Worse still, as the following example shows: even if
 the actual execution terminates, the analysis may not. The value of y keeps
-decreasing as the analysis is iterated, no matter how long:\<close>
+increasing as the analysis is iterated, no matter how long:\<close>
 
 value "show_acom (steps test4_ivl 50)"