src/HOL/IMP/Abs_Int3.thy
changeset 50995 3371f5ee4ace
parent 50986 c54ea7f5418f
child 51036 e7b54119c436
     1.1 --- a/src/HOL/IMP/Abs_Int3.thy	Sun Jan 20 15:34:27 2013 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int3.thy	Fri Jan 25 16:45:09 2013 +0100
     1.3 @@ -416,14 +416,14 @@
     1.4  value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))"
     1.5  value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))"
     1.6  value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))"
     1.7 -value "show_acom_opt (AI_ivl' test3_ivl)"
     1.8 +value "show_acom (the(AI_ivl' test3_ivl))"
     1.9  
    1.10  
    1.11  text{* Now all the analyses terminate: *}
    1.12  
    1.13 -value "show_acom_opt (AI_ivl' test4_ivl)"
    1.14 -value "show_acom_opt (AI_ivl' test5_ivl)"
    1.15 -value "show_acom_opt (AI_ivl' test6_ivl)"
    1.16 +value "show_acom (the(AI_ivl' test4_ivl))"
    1.17 +value "show_acom (the(AI_ivl' test5_ivl))"
    1.18 +value "show_acom (the(AI_ivl' test6_ivl))"
    1.19  
    1.20  
    1.21  subsubsection "Generic Termination Proof"