Re: [isabelle] isar-keywords

On Wed, 31 Mar 2010, Omar Montano Rivas wrote:

This is the ML code for the syntax,

val thms_parser = Scan.finite OuterLex.stopper (OuterParse.enum1 "," val add_rws_parser = OuterParse.reserved "add" -- OuterParse.$$$ ":" |-- thms_parser val del_rws_parser = OuterParse.reserved "del" -- OuterParse.$$$ ":" |-- thms_parser

val _ =
  OuterSyntax.command "modify_trs"
    "adds or deletes equations to the global term rewrite system"
    ((Scan.optional add_rws_parser [])
-- (Scan.optional del_rws_parser []) >> (fn (adds,dels) => Toplevel.theory (modify_TRS_cmd adds dels)))

The thms_parser with its own invocation of Scan.finite looks very odd -- it is probably imported from some of Christian Urban's examples on playing with the scanner framework independently from Isar outer syntax. If you just use (OuterParse.enum1 "," instead it should work.

Anyway, the whole modify_trs command looks like just a plain add/del declaration of theorems to the context. This can be done more conveniently and more flexibly via an "attribute", not a command.

Isar attributes can be used in many places, e.g. as follows

  declare blah [trs add]

or within a proof:

  note blah [trs del]

or more -- the above are just typical examples.

In Isabelle2009-1/src/Pure/Tools/named_thms.ML we have something like a canonical example of managing a plain list of theorems within the context, together with add/del attribute definition. The latter can also be done in Isar via the attribute_setup command. You can also use Named_Thms directly as a simplistic solution, if there are no special demands for indexing the content (although proper indexing is usually required for advanced tools).


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