Re: [isabelle] syntax issue in document preparation



Hi,

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

theory Scratch
imports Main
begin

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
test.induct}*}

end

Happy New Year
  Cornelius

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