equal
deleted
inserted
replaced
135 \end{isabelle} |
135 \end{isabelle} |
136 % |
136 % |
137 Applying this as an elimination rule yields one case where \isa{even.cases} |
137 Applying this as an elimination rule yields one case where \isa{even.cases} |
138 would yield two. Rule inversion works well when the conclusions of the |
138 would yield two. Rule inversion works well when the conclusions of the |
139 introduction rules involve datatype constructors like \isa{Suc} and \isa{\#} |
139 introduction rules involve datatype constructors like \isa{Suc} and \isa{\#} |
140 (list `cons'); freeness reasoning discards all but one or two cases. |
140 (list ``cons''); freeness reasoning discards all but one or two cases. |
141 |
141 |
142 In the \isacommand{inductive\_cases} command we supplied an |
142 In the \isacommand{inductive\_cases} command we supplied an |
143 attribute, \isa{elim!}, indicating that this elimination rule can be applied |
143 attribute, \isa{elim!}, indicating that this elimination rule can be applied |
144 aggressively. The original |
144 aggressively. The original |
145 \isa{cases} rule would loop if used in that manner because the |
145 \isa{cases} rule would loop if used in that manner because the |