[isabelle] syntax issue in document preparation



Hi,

in Nominal/Ex/Lambda.thy a proof command refers to path.induct . Now I
cannot use

   @{term path.induct}

in a proof document as it fails, but

   @{term path_induct}

which works but I wonder as it does not exist as a valid term.

Do I not understand something important about terms and antiquotations?

- Gergely




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.