| changeset 311 | 8b8db9558ecf |
| parent 307 | ee1caac29bb2 |
| child 330 | 89e6605c4ca4 |
| 310:c090baa7059d | 311:8b8db9558ecf |
|---|---|
1 |
1 |
2 theory Positions |
2 theory Positions |
3 imports "Spec" "Lexer" |
3 imports "Spec" "Lexer" |
4 begin |
4 begin |
5 |
|
6 chapter {* An alternative definition for POSIX values *} |
|
5 |
7 |
6 section {* Positions in Values *} |
8 section {* Positions in Values *} |
7 |
9 |
8 fun |
10 fun |
9 at :: "val \<Rightarrow> nat list \<Rightarrow> val" |
11 at :: "val \<Rightarrow> nat list \<Rightarrow> val" |