558 text {* 

   558 text {* 

   559   Now querying the definition you obtain:

   559   Now querying the definition you obtain:

   560 

   560 

   561   \begin{isabelle}

   561   \begin{isabelle}

   562   \isacommand{thm}~@{text "TrueConj_def"}\\

   562   \isacommand{thm}~@{text "TrueConj_def"}\\

   564   \end{isabelle}

   564   \end{isabelle}

   565 

   565 

   566   (FIXME give a better example why bindings are important; maybe

   566   (FIXME give a better example why bindings are important; maybe

   567   give a pointer to \isacommand{local\_setup})

   567   give a pointer to \isacommand{local\_setup})

   568 

   568