| changeset 48891 | c0eafbd55de3 |
| parent 46950 | d0181abdbdac |
| child 58825 | 2065f49da190 |
--- a/src/HOL/Statespace/StateSpaceLocale.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Statespace/StateSpaceLocale.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,9 +6,10 @@ theory StateSpaceLocale imports StateFun keywords "statespace" :: thy_decl -uses "state_space.ML" "state_fun.ML" begin +ML_file "state_space.ML" +ML_file "state_fun.ML" setup StateFun.setup text {* For every type that is to be stored in a state space, an