changeset 29247 | 95d3a82857e5 |
parent 29235 | 2d62b637fa80 |
child 38838 | 62f6ba39b3d4 |
--- a/src/HOL/Statespace/StateSpaceLocale.thy Tue Dec 16 21:11:39 2008 +0100 +++ b/src/HOL/Statespace/StateSpaceLocale.thy Thu Dec 18 11:16:48 2008 +0100 @@ -16,7 +16,7 @@ concrete values.*} -class_locale project_inject = +locale project_inject = fixes project :: "'value \<Rightarrow> 'a" and "inject":: "'a \<Rightarrow> 'value" assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"