| changeset 35182 | 4c39632b811f |
| parent 35181 | 92d857a4e5e0 |
| parent 35161 | be96405ccaf3 |
| child 35183 | 8580ba651489 |
| 35181:92d857a4e5e0 | 35182:4c39632b811f |
|---|---|
1 (* Author: Florian Haftmann, TU Muenchen *) |
|
2 |
|
3 header {* Index syntax for structures *} |
|
4 |
|
5 theory Structure_Syntax |
|
6 imports Pure |
|
7 begin |
|
8 |
|
9 syntax |
|
10 "_index1" :: index ("\<^sub>1") |
|
11 translations |
|
12 (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>" |
|
13 |
|
14 end |