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