equal
deleted
inserted
replaced
229 dest and elim rules are well-formed; dest and elim rules must have at |
229 dest and elim rules are well-formed; dest and elim rules must have at |
230 least one premise. |
230 least one premise. |
231 |
231 |
232 * Provers/classical: attributes dest/elim/intro take an optional |
232 * Provers/classical: attributes dest/elim/intro take an optional |
233 weight argument for the rule (just as the Pure versions). Weights are |
233 weight argument for the rule (just as the Pure versions). Weights are |
234 ignored by automated rules, but determine the search order of single |
234 ignored by automated tools, but determine the search order of single |
235 rule steps. |
235 rule steps. |
236 |
236 |
237 * Syntax: input syntax now supports dummy variable binding "%_. b", |
237 * Syntax: input syntax now supports dummy variable binding "%_. b", |
238 where the body does not mention the bound variable. Note that dummy |
238 where the body does not mention the bound variable. Note that dummy |
239 patterns implicitly depend on their context of bounds, which makes |
239 patterns implicitly depend on their context of bounds, which makes |