src/HOL/IMP/Abs_State.thy
changeset 50995 3371f5ee4ace
parent 49577 b199aa1d33fd
child 51036 e7b54119c436
     1.1 --- a/src/HOL/IMP/Abs_State.thy	Sun Jan 20 15:34:27 2013 +0100
     1.2 +++ b/src/HOL/IMP/Abs_State.thy	Fri Jan 25 16:45:09 2013 +0100
     1.3 @@ -109,7 +109,6 @@
     1.4  value [code] "show_st (FunDom (\<lambda>x. 1::int) {''a'',''b''})"
     1.5  
     1.6  definition "show_acom = map_acom (Option.map show_st)"
     1.7 -definition "show_acom_opt = Option.map show_acom"
     1.8  
     1.9  definition "update F x y = FunDom ((fun F)(x:=y)) (dom F)"
    1.10