--- a/src/HOL/IMP/Abs_Int1_const.thy Sun Jan 20 15:34:27 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy Fri Jan 25 16:45:09 2013 +0100
@@ -80,17 +80,17 @@
value "show_acom (steps test1_const 1)"
value "show_acom (steps test1_const 2)"
value "show_acom (steps test1_const 3)"
-value "show_acom_opt (AI_const test1_const)"
+value "show_acom (the(AI_const test1_const))"
-value "show_acom_opt (AI_const test2_const)"
-value "show_acom_opt (AI_const test3_const)"
+value "show_acom (the(AI_const test2_const))"
+value "show_acom (the(AI_const test3_const))"
value "show_acom (steps test4_const 0)"
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 (the(AI_const test4_const))"
value "show_acom (steps test5_const 0)"
value "show_acom (steps test5_const 1)"
@@ -99,7 +99,7 @@
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 (the(AI_const test5_const))"
value "show_acom (steps test6_const 0)"
value "show_acom (steps test6_const 1)"
@@ -115,7 +115,7 @@
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)"
+value "show_acom (the(AI_const test6_const))"
text{* Monotonicity: *}