--- a/src/HOL/IMP/Abs_Int3.thy Thu Sep 06 08:59:50 2012 -0700
+++ b/src/HOL/IMP/Abs_Int3.thy Fri Sep 07 07:20:55 2012 +0200
@@ -395,9 +395,13 @@
value "show_acom (step_up_ivl 3 (bot test3_ivl))"
value "show_acom (step_up_ivl 4 (bot test3_ivl))"
value "show_acom (step_up_ivl 5 (bot test3_ivl))"
-value "show_acom (step_down_ivl 1 (step_up_ivl 5 (bot test3_ivl)))"
-value "show_acom (step_down_ivl 2 (step_up_ivl 5 (bot test3_ivl)))"
-value "show_acom (step_down_ivl 3 (step_up_ivl 5 (bot test3_ivl)))"
+value "show_acom (step_up_ivl 6 (bot test3_ivl))"
+value "show_acom (step_up_ivl 7 (bot test3_ivl))"
+value "show_acom (step_up_ivl 8 (bot test3_ivl))"
+value "show_acom (step_down_ivl 1 (step_up_ivl 8 (bot test3_ivl)))"
+value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))"
+value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))"
+value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))"
value "show_acom_opt (AI_ivl' test3_ivl)"