src/HOL/Statespace/StateFun.thy
changeset 38838 62f6ba39b3d4
parent 35416 d8d7d1b785af
child 41959 b460124855b8
     1.1 --- a/src/HOL/Statespace/StateFun.thy	Fri Aug 27 22:09:51 2010 +0200
     1.2 +++ b/src/HOL/Statespace/StateFun.thy	Fri Aug 27 22:30:25 2010 +0200
     1.3 @@ -33,10 +33,10 @@
     1.4  lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
     1.5    by (rule refl)
     1.6  
     1.7 -definition lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
     1.8 +definition lookup :: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
     1.9    where "lookup destr n s = destr (s n)"
    1.10  
    1.11 -definition update::
    1.12 +definition update ::
    1.13    "('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
    1.14    where "update destr constr n f s = s(n := constr (f (destr (s n))))"
    1.15