891   @{ML_ind define in Local_Theory}.  This function is used below to define 

   891   @{ML_ind define in Local_Theory}.  This function is used below to define 

   892   the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.

   892   the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.

   893 *}

   893 *}

   894 

   894 

   895 local_setup %gray {* 

   895 local_setup %gray {* 

   897       (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *}

   897       (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *}

   898 

   898 

   899 text {* 

   899 text {* 

   900   Now querying the definition you obtain:

   900   Now querying the definition you obtain:

   901 

   901