[isabelle] Antiqutation for Theorem names

Hi again!

I tried to build my own antiquotation for doing what I indicated in my last mail and came up with the following code:

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

fun output_thm_name {context = ctxt, ...} names =
  let val _ =
    map (PureThy.get_thm (ProofContext.theory_of ctxt)) names
    ThyOutput.output [Pretty.block (output_names names)]

val _ = ThyOutput.antiquotation "lemmas"
  (Scan.repeat1 (Scan.lift Args.name)) output_thm_name

text {*
Some theorems are: @{lemmas conjI disjE impI}. Or @{lemmas FalseE}

My remaining question would be: How do I indicate, that the word "and" should be printed as standard text?



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