[isabelle] Which parser to use for theorems in a toplevel-command?
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Which parser to use for theorems in a toplevel-command?
- From: Lars Noschinski <noschinl at in.tum.de>
- Date: Mon, 26 Aug 2013 11:13:13 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.12) Gecko/20130116 Icedove/10.0.12
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and