2096 @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}. |
2096 @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}. |
2097 |
2097 |
2098 Note also that applications of \<open>assumption\<close> do not |
2098 Note also that applications of \<open>assumption\<close> do not |
2099 count as a separate theorem, as you can see in the following code. |
2099 count as a separate theorem, as you can see in the following code. |
2100 |
2100 |
2101 @{ML_matchresult [display,gray] |
2101 @{ML_response [display,gray] |
2102 \<open>@{thm my_conjIb} |
2102 \<open>@{thm my_conjIb} |
2103 |> get_all_names |> sort string_ord\<close> |
2103 |> get_all_names |> sort string_ord\<close> |
2104 \<open>["", "Pure.protectD", "Pure.protectI"]\<close>} |
2104 \<open>[ "Pure.protectD", "Pure.protectI"]\<close>} |
2105 |
2105 |
2106 |
2106 |
2107 Interestingly, but not surprisingly, the proof of @{thm [source] |
2107 Interestingly, but not surprisingly, the proof of @{thm [source] |
2108 my_conjIc} procceeds quite differently from @{thm [source] my_conjIa} |
2108 my_conjIc} procceeds quite differently from @{thm [source] my_conjIa} |
2109 and @{thm [source] my_conjIb}, as can be seen by the theorems that |
2109 and @{thm [source] my_conjIb}, as can be seen by the theorems that |