[isabelle] Obtaining a list of theorems in ML



Hello,

I am interested in obtaining the theorems declared in a certain context.
I know that I can get these theorems from the current context using
anti-quotations @{thms MyTh}. However this is not satisfactory because
I need these theorems from a dynamic context which is passed as an
argument to a function.

So I need a function "GetMyThms ctxt" which does exactly the same
as @{thms MyTh}, but for ctxt parameter, and not the current context.

theorems MyTh = exI exE

ML{*
val my_ths = @{thms MyTh};
val ctxt = @{context}

fun GetMyThms ctxt = ..;
val my_thsa = GetMyThms ctxt;
*}

How can I achieve this?

Best regards,

Viorel Preoteasa




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