| changeset 46950 | d0181abdbdac |
| parent 45358 | 4849133d7a78 |
| child 48891 | c0eafbd55de3 |
--- a/src/HOL/Statespace/StateSpaceLocale.thy Thu Mar 15 20:07:00 2012 +0100 +++ b/src/HOL/Statespace/StateSpaceLocale.thy Thu Mar 15 22:08:53 2012 +0100 @@ -5,6 +5,7 @@ header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*} theory StateSpaceLocale imports StateFun +keywords "statespace" :: thy_decl uses "state_space.ML" "state_fun.ML" begin