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.$$$ ":" |--
val del_rws_parser = OuterParse.reserved "del" -- OuterParse.$$$ ":" |--
val _ =
"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 "," OuterParse.name) 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and