Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Statespace/StateSpaceLocale.thy
changeset 29235 2d62b637fa80
parent 25174 d70d6dbc3a60
child 29247 95d3a82857e5 
--- a/src/HOL/Statespace/StateSpaceLocale.thy	Mon Dec 15 18:12:52 2008 +0100
+++ b/src/HOL/Statespace/StateSpaceLocale.thy	Tue Dec 16 15:09:12 2008 +0100
@@ -16,7 +16,7 @@
 concrete values.*}
 
 
-locale project_inject =
+class_locale project_inject =
  fixes project :: "'value \<Rightarrow> 'a"
  and   "inject":: "'a \<Rightarrow> 'value"
  assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
isabelle