| changeset 60592 | c9bd1d902f04 |
| parent 60590 | 479071e8778f |
| child 62145 | 5b946c81dfbf |
| 60591:e0b77517f9a9 | 60592:c9bd1d902f04 |
|---|---|
1 (* Title: HOL/TLA/Stfun.thy |
1 (* Title: HOL/TLA/Stfun.thy |
2 Author: Stephan Merz |
2 Author: Stephan Merz |
3 Copyright: 1998 University of Munich |
3 Copyright: 1998 University of Munich |
4 *) |
4 *) |
5 |
5 |
6 section {* States and state functions for TLA as an "intensional" logic *} |
6 section \<open>States and state functions for TLA as an "intensional" logic\<close> |
7 |
7 |
8 theory Stfun |
8 theory Stfun |
9 imports Intensional |
9 imports Intensional |
10 begin |
10 begin |
11 |
11 |