equal
deleted
inserted
replaced
840 It is also possible to prove lemmas with the antiquotation @{text "@{lemma \<dots> by \<dots>}"} |
840 It is also possible to prove lemmas with the antiquotation @{text "@{lemma \<dots> by \<dots>}"} |
841 whose first argument is a statement (possibly many of them separated by @{text "and"}) |
841 whose first argument is a statement (possibly many of them separated by @{text "and"}) |
842 and the second is a proof. For example |
842 and the second is a proof. For example |
843 *} |
843 *} |
844 |
844 |
845 ML{*val foo_thm = @{lemma "True" and "True" by simp simp} *} |
845 ML{*val foo_thm = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *} |
846 |
846 |
847 text {* |
847 text {* |
848 The result can be printed out as follows. |
848 The result can be printed out as follows. |
849 |
849 |
850 @{ML_response_fake [gray,display] |
850 @{ML_response_fake [gray,display] |