equal
deleted
inserted
replaced
186 src/HOL/Library/Coinductive_List.thy for various examples. |
186 src/HOL/Library/Coinductive_List.thy for various examples. |
187 |
187 |
188 * Provers/classical: removed obsolete classical version of elim_format |
188 * Provers/classical: removed obsolete classical version of elim_format |
189 attribute; classical elim/dest rules are now treated uniformly when |
189 attribute; classical elim/dest rules are now treated uniformly when |
190 manipulating the claset. |
190 manipulating the claset. |
|
191 |
|
192 * Provers/classical: stricter checks to ensure that supplied intro, dest and |
|
193 elim rules are well-formed; dest and elim rules must have at least one premise. |
191 |
194 |
192 * Syntax: input syntax now supports dummy variable binding "%_. b", |
195 * Syntax: input syntax now supports dummy variable binding "%_. b", |
193 where the body does not mention the bound variable. Note that dummy |
196 where the body does not mention the bound variable. Note that dummy |
194 patterns implicitly depend on their context of bounds, which makes |
197 patterns implicitly depend on their context of bounds, which makes |
195 "{_. _}" match any set comprehension as expected. Potential |
198 "{_. _}" match any set comprehension as expected. Potential |