equal
deleted
inserted
replaced
185 |
185 |
186 |
186 |
187 (* concrete syntax *) |
187 (* concrete syntax *) |
188 |
188 |
189 val rule_atts = |
189 val rule_atts = |
190 [("dest", (Attrib.no_args dest_global, Attrib.no_args dest_local), "destruction rule"), |
190 [("dest", (Attrib.no_args dest_global, Attrib.no_args dest_local), "declare destruction rule"), |
191 ("elim", (Attrib.no_args elim_global, Attrib.no_args elim_local), "elimination rule"), |
191 ("elim", (Attrib.no_args elim_global, Attrib.no_args elim_local), "declare elimination rule"), |
192 ("intro", (Attrib.no_args intro_global, Attrib.no_args intro_local), "introduction rule"), |
192 ("intro", (Attrib.no_args intro_global, Attrib.no_args intro_local), "declare introduction rule"), |
193 ("delrule", (Attrib.no_args delrule_global, Attrib.no_args delrule_local), "delete rule")]; |
193 ("delrule", (Attrib.no_args delrule_global, Attrib.no_args delrule_local), "undeclare rule")]; |
194 |
194 |
195 |
195 |
196 |
196 |
197 (** proof methods **) |
197 (** proof methods **) |
198 |
198 |