| changeset 27015 | f8537d69f514 |
| parent 18724 | cb6e0064c88c |
| 27014:a5f53d9d2b60 | 27015:f8537d69f514 |
|---|---|
70 *} |
70 *} |
71 |
71 |
72 consts M :: "(state \<times> state)set"; |
72 consts M :: "(state \<times> state)set"; |
73 |
73 |
74 text{*\noindent |
74 text{*\noindent |
75 Again, we could have made @{term M} a parameter of everything. |
75 This is Isabelle's way of declaring a constant without defining it. |
76 Finally we introduce a type of atomic propositions |
76 Finally we introduce a type of atomic propositions |
77 *} |
77 *} |
78 |
78 |
79 typedecl "atom" |
79 typedecl "atom" |
80 |
80 |