[isabelle] Which parser to use for theorems in a toplevel-command?


I want to write a toplevel command which takes a theorem and some options as input and creates a list of theorems (hence I cannot use an attribute) from that.

In an attribute I would use the Attrib.thm parser to parse the input theorem. Is Parse_Spec.xthm the right thing to use in a command, or is there something more ready-made, where I don't need to care about applying the attributes myself?

  -- Lars

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