836   makes your code independent from what theorems the user might have stored

   836   makes your code independent from what theorems the user might have stored

   837   under this name (this becomes especially important when you deal with

   837   under this name (this becomes especially important when you deal with

   838   theorem lists; see Section \ref{sec:storing}).

   838   theorem lists; see Section \ref{sec:storing}).

   839 

   839 

   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>}"}

   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 "True" by simp simp} *}

   846 

   846