*To*: Viorel Preoteasa <viorel.preoteasa at aalto.fi>*Subject*: Re: [isabelle] Obtaining a list of theorems in ML*From*: Makarius <makarius at sketis.net>*Date*: Tue, 1 Sep 2015 21:16:48 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <55E5CF3B.6060405@aalto.fi>*References*: <55E4A2B5.1080300@wanadoo.fr> <55E5B0CC.7060803@aalto.fi> <alpine.LNX.2.00.1509011733270.23875@lxbroy10.informatik.tu-muenchen.de> <55E5CF3B.6060405@aalto.fi>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 1 Sep 2015, Viorel Preoteasa wrote:

For example, dynamically changing facts can be managed like this in Isabelle2015: named_theorems foo ML âfun get_foo ctxt = Named_Theorems.get ctxt @{named_theorems foo}â The user can now use attributes [foo add] or [foo del]. Your tool can use get_foo to see the current content in a given context.This is a nice solution. Is there a way to also clear the foo content,without knowing what it contains?

setup âGlobal_Theory.add_thms_dynamic (@{binding foo}, undefined)â

Makarius

**References**:**[isabelle] Obtaining a list of theorems in ML***From:*Viorel Preoteasa

**Re: [isabelle] Obtaining a list of theorems in ML***From:*Makarius

**Re: [isabelle] Obtaining a list of theorems in ML***From:*Viorel Preoteasa

- Previous by Date: Re: [isabelle] Obtaining a list of theorems in ML
- Next by Date: [isabelle] strange type inference
- Previous by Thread: Re: [isabelle] Obtaining a list of theorems in ML
- Next by Thread: [isabelle] strange type inference
- Cl-isabelle-users September 2015 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