equal
deleted
inserted
replaced
67 local |
67 local |
68 |
68 |
69 val introN = "intro"; |
69 val introN = "intro"; |
70 val elimN = "elim"; |
70 val elimN = "elim"; |
71 val destN = "dest"; |
71 val destN = "dest"; |
72 val ruleN = "rule"; |
|
73 |
72 |
74 fun modifier name kind kind' att = |
73 fun modifier name kind kind' att = |
75 Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME) |
74 Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME) |
76 >> (pair (I: Proof.context -> Proof.context) o att); |
75 >> (pair (I: Proof.context -> Proof.context) o att); |
77 |
76 |