equal
deleted
inserted
replaced
794 @{ML_response_fake [display,gray] |
794 @{ML_response_fake [display,gray] |
795 "[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}" |
795 "[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}" |
796 "\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)"} |
796 "\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)"} |
797 |
797 |
798 If you need to instantiate lists of theorems, you can use the |
798 If you need to instantiate lists of theorems, you can use the |
799 functions @{ML_ind RL in Drule} and @{ML_ind MRL in Drule}. For |
799 functions @{ML_ind RL in Drule} and @{ML_ind OF in Drule}. For |
800 example in the code below, every theorem in the second list is |
800 example in the code below, every theorem in the second list is |
801 instantiated with every theorem in the first. |
801 instantiated with every theorem in the first. |
802 |
802 |
803 @{ML_response_fake [display,gray] |
803 @{ML_response_fake [display,gray] |
804 "let |
804 "let |