Re: [isabelle] syntax issue in document preparation


In my Isabelle2014, I did not find the file, so I tried to reproduce a
minimal example for you.

theory Scratch
imports Main

fun test :: "nat ⇒ nat" where
  "test 0 = 0" |
  "test (Suc n) = test n"

text{*Undefined constant: @{term test.induct}.*} (*Isabelle2014
highlights the error in jEdit, without running latex*)
text{*You can use the term antiquotation to display terms: @{term
"test 0 = 0"} *}
text{*The term antiquotation checks for errors: @{term "test 0 = -1"}
*} (*Type unification failed: No type arity nat :: uminus*)
text{*You can use the text antiquotation to do things without checks:
@{text "test 0 = -1"}*}
thm test.induct
text{*If you want to reference facts (things you can also view with
the thm command in Isabelle), use the thm antiquotation: @{thm


Happy New Year

2014-12-30 17:35 GMT+01:00 Gergely Buday <gbuday at>:
> 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.