176   Hint: The third term is already quite big, and the pretty printer

   176   Hint: The third term is already quite big, and the pretty printer

   177   may omit parts of it by default. If you want to see all of it, you

   177   may omit parts of it by default. If you want to see all of it, you

   178   can use the following ML-function to set the printing depth to a higher 

   178   can use the following ML-function to set the printing depth to a higher 

   179   value:

   179   value:

   180 

   180 

   182   \end{exercise}

   182   \end{exercise}

   183 

   183 

   184   The antiquotation @{text "@{prop \<dots>}"} constructs terms by inserting the 

   184   The antiquotation @{text "@{prop \<dots>}"} constructs terms by inserting the 

   185   usually invisible @{text "Trueprop"}-coercions whenever necessary. 

   185   usually invisible @{text "Trueprop"}-coercions whenever necessary. 

   186   Consider for example the pairs

   186   Consider for example the pairs