[isabelle] Storing Data and naming theorems in ML



Hello again,

I've got another few implementational questions, just to make sure I get things the right way around.

1) My application discovers and proves some new lemmas that it thinks might be useful, so these need to be stored suitably, in some Theory_Data for the current theory. So far so good, following the instructions in section 2.5 of the Isabelle Cookbook/programming tutorial. However, I would like to be able to update my collection of useful lemmas programatically, but in the tutorial, it is only shown how to do this using the Isar command "setup", e.g. as below:

setup {* Context.theory_map (FooRules.add_thm @{thm TrueI}) *}

Presumably there must be an ML function corresponding to setup somewhere?


2) I would like to also give individual nice names to my automatically discovered lemmas. What is the procedure for doing this?


Thanks,
Moa




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