src/HOL/Statespace/StateFun.thy
changeset 35416 d8d7d1b785af
parent 35114 b1fd1d756e20
child 38838 62f6ba39b3d4
--- a/src/HOL/Statespace/StateFun.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Statespace/StateFun.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -22,7 +22,7 @@
 better compositionality, especially if you think of nested state
 spaces.  *} 
 
-constdefs K_statefun:: "'a \<Rightarrow> 'b \<Rightarrow> 'a" "K_statefun c x \<equiv> c"
+definition K_statefun :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where "K_statefun c x \<equiv> c"
 
 lemma K_statefun_apply [simp]: "K_statefun c x = c"
   by (simp add: K_statefun_def)