| changeset 22378 | 8e02a61b401f |
| parent 22362 | 6470ce514b6e |
| child 22682 | 92448396c9d9 |
| 22377:61610b1beedf | 22378:8e02a61b401f |
|---|---|
74 val lemmaK = "lemma"; |
74 val lemmaK = "lemma"; |
75 val corollaryK = "corollary"; |
75 val corollaryK = "corollary"; |
76 val internalK = "internal"; |
76 val internalK = "internal"; |
77 |
77 |
78 |
78 |
79 |
|
80 (* attributes *) |
79 (* attributes *) |
81 |
80 |
82 fun rule_attribute f (x, th) = (x, f x th); |
81 fun rule_attribute f (x, th) = (x, f x th); |
83 fun declaration_attribute f (x, th) = (f th x, th); |
82 fun declaration_attribute f (x, th) = (f th x, th); |
84 |
83 |