681   for constructing the terms for the logical connectives.\footnote{Thanks to Roy

   681   for constructing the terms for the logical connectives.\footnote{Thanks to Roy

   682   Dyckhoff for suggesting this exercise and working out the details.} 

   682   Dyckhoff for suggesting this exercise and working out the details.} 

   683   \end{exercise}

   683   \end{exercise}

   684 *}

   684 *}

   685 

   685 

   687 

   687 

   688 text {* 

   688 text {* 

   689   As seen earlier, Isabelle's terms and types may contain schematic term variables

   689   As seen earlier, Isabelle's terms and types may contain schematic term variables

   690   (term-constructor @{ML Var}) and schematic type variables (term-constructor

   690   (term-constructor @{ML Var}) and schematic type variables (term-constructor

   691   @{ML TVar}). These variables stand for unknown entities, which can be made

   691   @{ML TVar}). These variables stand for unknown entities, which can be made