| changeset 58889 | 5b7a9633cfa8 |
| parent 56256 | 1e01c159e7d9 |
| child 59498 | 50b60f501b05 |
| 58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
|---|---|
1 (* Title: HOL/TLA/Action.thy |
1 (* Title: HOL/TLA/Action.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 header {* The action level of TLA as an Isabelle theory *} |
6 section {* The action level of TLA as an Isabelle theory *} |
7 |
7 |
8 theory Action |
8 theory Action |
9 imports Stfun |
9 imports Stfun |
10 begin |
10 begin |
11 |
11 |