| changeset 55382 | 9218fa411c15 |
| parent 42018 | 878f33040280 |
| child 58889 | 5b7a9633cfa8 |
| 55381:ca31f042414f | 55382:9218fa411c15 |
|---|---|
8 theory Stfun |
8 theory Stfun |
9 imports Intensional |
9 imports Intensional |
10 begin |
10 begin |
11 |
11 |
12 typedecl state |
12 typedecl state |
13 |
13 instance state :: world .. |
14 arities state :: world |
|
15 |
14 |
16 type_synonym 'a stfun = "state => 'a" |
15 type_synonym 'a stfun = "state => 'a" |
17 type_synonym stpred = "bool stfun" |
16 type_synonym stpred = "bool stfun" |
18 |
17 |
19 |
18 |