# HG changeset patch
# User nipkow
# Date 1368696454 -7200
# Node ID e0a83bd90bb1fcfe753d12811369ccaf8d23d77c
# Parent  59963cda805a8f34b6c6dd1426dd3aefa0810289
tuned

diff -r 59963cda805a -r e0a83bd90bb1 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Thu May 16 13:49:18 2013 +1000
+++ b/src/HOL/IMP/Abs_Int0.thy	Thu May 16 11:27:34 2013 +0200
@@ -480,6 +480,6 @@
 end
 
 text{* Problem: not executable because of the comparison of abstract states,
-i.e. functions, in the post-fixedpoint computation. *}
+i.e. functions, in the pre-fixpoint computation. *}
 
 end