changeset 44762 | 8f9d09241a68 |
parent 41959 | b460124855b8 |
child 45358 | 4849133d7a78 |
--- a/src/HOL/Statespace/StateFun.thy Tue Sep 06 13:16:46 2011 -0700 +++ b/src/HOL/Statespace/StateFun.thy Wed Sep 07 00:08:09 2011 +0200 @@ -28,7 +28,7 @@ by (simp add: K_statefun_def) lemma K_statefun_comp [simp]: "(K_statefun c \<circ> f) = K_statefun c" - by (rule ext) (simp add: K_statefun_apply comp_def) + by (rule ext) (simp add: comp_def) lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x" by (rule refl)