equal
deleted
inserted
replaced
2204 |
2204 |
2205 definition id2::"'a \<Rightarrow> 'a" |
2205 definition id2::"'a \<Rightarrow> 'a" |
2206 where "id2 \<equiv> \<lambda>x. x" |
2206 where "id2 \<equiv> \<lambda>x. x" |
2207 |
2207 |
2208 text {* |
2208 text {* |
2209 Both definitions define the same function, although the theorems @{thm |
2209 Although both definitions define the same function, the theorems @{thm |
2210 [source] id1_def} and @{thm [source] id2_def} are different. However it is |
2210 [source] id1_def} and @{thm [source] id2_def} are different. However it is |
2211 easy to transform one theorem into the other. The function @{ML_ind abs_def |
2211 easy to transform one theorem into the other. The function @{ML_ind abs_def |
2212 in Drule} can automatically transform theorem @{thm [source] id1_def} |
2212 in Drule} can automatically transform theorem @{thm [source] id1_def} |
2213 into @{thm [source] id2_def} by abstracting all variables on the |
2213 into @{thm [source] id2_def} by abstracting all variables on the |
2214 left-hand side in the right-hand side. |
2214 left-hand side in the right-hand side. |