# HG changeset patch
# User nipkow
# Date 1327042543 -3600
# Node ID 0bacd41ce2482a5f7f3e45ad24de3c52b23cd68e
# Parent  adf10579fe434391d480fa8fa80080412c0cfaff
tuned

diff -r adf10579fe43 -r 0bacd41ce248 src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Thu Jan 19 21:37:12 2012 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Fri Jan 20 07:55:43 2012 +0100
@@ -238,23 +238,23 @@
 definition "step_down_ivl n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> c)^^n)"
 
 text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
-the loop took to execute. In contrast, @{const AI_ivl} converges in a
+the loop took to execute. In contrast, @{const AI_ivl'} converges in a
 constant number of steps: *}
 
-value [code] "show_acom (step_up_ivl 1 (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (step_up_ivl 2 (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (step_up_ivl 3 (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (step_up_ivl 4 (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (step_down_ivl 1 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
-value [code] "show_acom (step_down_ivl 2 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
-value [code] "show_acom (step_down_ivl 3 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
+value "show_acom (step_up_ivl 1 (\<bottom>\<^sub>c test3_ivl))"
+value "show_acom (step_up_ivl 2 (\<bottom>\<^sub>c test3_ivl))"
+value "show_acom (step_up_ivl 3 (\<bottom>\<^sub>c test3_ivl))"
+value "show_acom (step_up_ivl 4 (\<bottom>\<^sub>c test3_ivl))"
+value "show_acom (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl))"
+value "show_acom (step_down_ivl 1 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
+value "show_acom (step_down_ivl 2 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
+value "show_acom (step_down_ivl 3 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
 
 text{* Now all the analyses terminate: *}
 
-value [code] "show_acom_opt (AI_ivl' test4_ivl)"
-value [code] "show_acom_opt (AI_ivl' test5_ivl)"
-value [code] "show_acom_opt (AI_ivl' test6_ivl)"
+value "show_acom_opt (AI_ivl' test4_ivl)"
+value "show_acom_opt (AI_ivl' test5_ivl)"
+value "show_acom_opt (AI_ivl' test6_ivl)"
 
 
 subsubsection "Termination: Intervals"