Re: [isabelle] Antiquotation for Theorem Names



Hi Chris,

In the meantime I modified my antiquotation function as follows

[...]

  let
    val _ = map (PureThy.get_fact (Context.Proof ctxt)
     (ProofContext.theory_of ctxt) o Facts.named) names

this only takes the facts from the theory. Did you try something like
ProofContext.get_fact(s) / .get_thm(s) ?

Alex





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