*To*: Ognjen Maric <ognjen.maric at gmail.com>*Subject*: Re: [isabelle] Storing theorems on the fly*From*: Makarius <makarius at sketis.net>*Date*: Wed, 28 Nov 2012 13:44:14 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50B5FA16.8090607@gmail.com>*References*: <50B5FA16.8090607@gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Wed, 28 Nov 2012, Ognjen Maric wrote:

A single subterm might appear many times, and I'd like to store thegenerated theorems to avoid repeating the work.

Clearly, they could be manually threaded through the recursive calls,but I'd like to avoid doing the plumbing myself, especially since I'dlike to be able to retrieve them later (outside of the function) aswell.So I assume I should be using one of the context.*_Data structures to store the theorems in an Item_Net (indexed by the terms). Questions: Questions: 1. Right now I'm trying to do this from an ML {* *} block within Isar text, using Generic_Data and then storing the generated theorems with Context.>>. However, it appears that the theorems only actually get stored after the whole ML {* *} block is executed. Is this a feature, and if so, how to get around to it?

What are you trying to achieve concretely?

2. Could this be done within a proof tactic, and how?

Makarius

**Follow-Ups**:**Re: [isabelle] Storing theorems on the fly***From:*Ognjen Maric

**References**:**[isabelle] Storing theorems on the fly***From:*Ognjen Maric

- Previous by Date: [isabelle] Storing theorems on the fly
- Next by Date: Re: [isabelle] Storing theorems on the fly
- Previous by Thread: [isabelle] Storing theorems on the fly
- Next by Thread: Re: [isabelle] Storing theorems on the fly
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list