| changeset 35118 | 724e8f77806a |
| parent 35117 | eeec2a320a77 |
| parent 35116 | 133be405a6f1 |
| child 35119 | b271a8996f26 |
| 35117:eeec2a320a77 | 35118:724e8f77806a |
|---|---|
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 |