changeset 27065 | f68aa7b5a0f3 |
parent 26967 | 27f60aaa5a7b |
child 27189 | 1a9b9da1c0d7 |
27064:267cab537760 | 27065:f68aa7b5a0f3 |
---|---|
4 theory Classes |
4 theory Classes |
5 imports Main Code_Integer |
5 imports Main Code_Integer |
6 begin |
6 begin |
7 |
7 |
8 ML {* |
8 ML {* |
9 CodeTarget.code_width := 74; |
9 CodeTarget.target_code_width := 74; |
10 *} |
10 *} |
11 |
11 |
12 syntax |
12 syntax |
13 "_alpha" :: "type" ("\<alpha>") |
13 "_alpha" :: "type" ("\<alpha>") |
14 "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()\<Colon>_" [0] 1000) |
14 "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()\<Colon>_" [0] 1000) |