| changeset 51711 | df3426139651 |
| parent 51389 | 8a9f0503b1c0 |
| child 51801 | 1006b9b08d73 |
--- a/src/HOL/IMP/Abs_Int1_const.thy Wed Apr 17 20:53:26 2013 +0200 +++ b/src/HOL/IMP/Abs_Int1_const.thy Wed Apr 17 21:11:01 2013 +0200 @@ -80,7 +80,7 @@ subsubsection "Tests" -definition "steps c i = (step_const(Top(vars c)) ^^ i) (bot c)" +definition "steps c i = (step_const \<top> ^^ i) (bot c)" value "show_acom (steps test1_const 0)" value "show_acom (steps test1_const 1)"