equal
deleted
inserted
replaced
1 (* Title: StateSpaceEx.thy |
1 (* Title: StateSpaceEx.thy |
2 ID: $Id$ |
|
3 Author: Norbert Schirmer, TU Muenchen |
2 Author: Norbert Schirmer, TU Muenchen |
4 *) |
3 *) |
5 |
4 |
6 header {* Examples \label{sec:Examples} *} |
5 header {* Examples \label{sec:Examples} *} |
7 theory StateSpaceEx |
6 theory StateSpaceEx |
8 imports StateSpaceLocale StateSpaceSyntax |
7 imports StateSpaceLocale StateSpaceSyntax |
9 |
|
10 begin |
8 begin |
11 (* FIXME: Use proper keywords file *) |
9 |
12 (*<*) |
10 (*<*) |
13 syntax |
11 syntax |
14 "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_\<langle>_\<rangle>" [900,0] 900) |
12 "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_\<langle>_\<rangle>" [900,0] 900) |
15 (*>*) |
13 (*>*) |
16 |
14 |