equal
deleted
inserted
replaced
4 |
4 |
5 header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*} |
5 header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*} |
6 |
6 |
7 theory StateSpaceLocale imports StateFun |
7 theory StateSpaceLocale imports StateFun |
8 keywords "statespace" :: thy_decl |
8 keywords "statespace" :: thy_decl |
9 uses "state_space.ML" "state_fun.ML" |
|
10 begin |
9 begin |
11 |
10 |
|
11 ML_file "state_space.ML" |
|
12 ML_file "state_fun.ML" |
12 setup StateFun.setup |
13 setup StateFun.setup |
13 |
14 |
14 text {* For every type that is to be stored in a state space, an |
15 text {* For every type that is to be stored in a state space, an |
15 instance of this locale is imported in order convert the abstract and |
16 instance of this locale is imported in order convert the abstract and |
16 concrete values.*} |
17 concrete values.*} |