Gergely Buday
2014-12-30 16:42:17 UTC
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
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