# HG changeset patch
# User nipkow
# Date 1346995255 -7200
# Node ID 22f7e7b68f50b4e93888061f6cee31d44d51bb29
# Parent  6096da55d2d6d881053cf637a5ea28a0d2b0b98f
adjusted examples

diff -r 6096da55d2d6 -r 22f7e7b68f50 src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thy	Thu Sep 06 08:59:50 2012 -0700
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Fri Sep 07 07:20:55 2012 +0200
@@ -89,6 +89,7 @@
 value "show_acom (steps test4_const 1)"
 value "show_acom (steps test4_const 2)"
 value "show_acom (steps test4_const 3)"
+value "show_acom (steps test4_const 4)"
 value "show_acom_opt (AI_const test4_const)"
 
 value "show_acom (steps test5_const 0)"
@@ -97,6 +98,7 @@
 value "show_acom (steps test5_const 3)"
 value "show_acom (steps test5_const 4)"
 value "show_acom (steps test5_const 5)"
+value "show_acom (steps test5_const 6)"
 value "show_acom_opt (AI_const test5_const)"
 
 value "show_acom (steps test6_const 0)"
@@ -111,6 +113,8 @@
 value "show_acom (steps test6_const 9)"
 value "show_acom (steps test6_const 10)"
 value "show_acom (steps test6_const 11)"
+value "show_acom (steps test6_const 12)"
+value "show_acom (steps test6_const 13)"
 value "show_acom_opt (AI_const test6_const)"
 
 
diff -r 6096da55d2d6 -r 22f7e7b68f50 src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Thu Sep 06 08:59:50 2012 -0700
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Fri Sep 07 07:20:55 2012 +0200
@@ -136,6 +136,7 @@
 value "show_acom (steps test2_parity 3)"
 value "show_acom (steps test2_parity 4)"
 value "show_acom (steps test2_parity 5)"
+value "show_acom (steps test2_parity 6)"
 value "show_acom_opt (AI_parity test2_parity)"
 
 
diff -r 6096da55d2d6 -r 22f7e7b68f50 src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Thu Sep 06 08:59:50 2012 -0700
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Fri Sep 07 07:20:55 2012 +0200
@@ -261,6 +261,7 @@
 value "show_acom (steps test2_ivl 0)"
 value "show_acom (steps test2_ivl 1)"
 value "show_acom (steps test2_ivl 2)"
+value "show_acom (steps test2_ivl 3)"
 
 text{* Fixed point reached in 2 steps.
  Not so if the start value of x is known: *}
@@ -271,6 +272,7 @@
 value "show_acom (steps test3_ivl 2)"
 value "show_acom (steps test3_ivl 3)"
 value "show_acom (steps test3_ivl 4)"
+value "show_acom (steps test3_ivl 5)"
 
 text{* Takes as many iterations as the actual execution. Would diverge if
 loop did not terminate. Worse still, as the following example shows: even if
diff -r 6096da55d2d6 -r 22f7e7b68f50 src/HOL/IMP/Abs_Int3.thy
--- 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)"