articles and slides usually do not include the formal content in

   articles and slides usually do not include the formal content in

   full.  Delimiting \bfindex{ignored material} by the special source

   full.  Delimiting \bfindex{ignored material} by the special source

   comments \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and

   comments \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and

   \verb,(,\verb,*,\verb,>,\verb,*,\verb,), tells the document

   \verb,(,\verb,*,\verb,>,\verb,*,\verb,), tells the document

   preparation system to suppress these parts; the formal checking of

   preparation system to suppress these parts; the formal checking of

   In this example, we hide a theory's \isakeyword{theory} and

   In this example, we hide a theory's \isakeyword{theory} and

   \isakeyword{end} brackets:

   \isakeyword{end} brackets:

   \medskip

   \medskip