[isabelle] Antiquotation for Theorem Names



Hi!

In the meantime I modified my antiquotation function as follows

fun output_names [name] = [Pretty.str name]
| output_names [n1, n2] = [Pretty.str n1, Pretty.str " and ", Pretty.str n2]
  | output_names names =
    let val (ns, n) = split_last (map Pretty.str names) in
      Pretty.commas ns @ [Pretty.str ", and ", n]
    end

fun output_thm_names
  ({context = ctxt, ...} : {state : Toplevel.state, source : Args.src,
    context: Proof.context})
  names =
  let
    val _ = map (PureThy.get_fact (Context.Proof ctxt)
     (ProofContext.theory_of ctxt) o Facts.named) names
  in
    ThyOutput.output [Pretty.block (output_names names)]
  end

This works in principle (for single names). E.g.,

lemma bla: ...

text {* @{lemmas bla} *}

produces "bla" in the resulting pdf. However, this does not work for 'local facts'. E.g.,

...
case (Suc n)
txt {* @{lemmas Suc} *}

results in the error: *** Unknown fact "Suc"

Is it impossible to refer to 'local facts' in antiquotations?

cheers

chris





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