[isabelle-dev] Theory.get_name

Christian Sternagel christian.sternagel at gmail.com
Thu Aug 20 08:10:58 CEST 2009

This can be done via 'Context.thoery_name : theory -> string'. I used 
'grep' to find this function

   $ grep -R 'val' /usr/local/Isabelle/src/ | grep ':' | \
     grep 'string$' | grep theory | less

I.e., i searched in all of Isabelle sources for some function signature 
(starting with 'val' and containing a ':' before the type) who's result 
type (assuming that this is written at the end of the line) is 'string' 
and there is also 'theory' contained somewhere. I always build these 
piped greps incrementally until I no longer get to many results.

It's very easy to find functions this way.



On 08/19/2009 08:57 PM, Walther Neuper wrote:
> Hi all,
> migrating code based on a _very_ old version of Isabelle to
> Isabelle2009, I'm happy with the many improvements.
> Our code switches between object-language (e.g.theory, thm) and
> meta-language (i.e.string) and thus we need
> ML> Thm.get_name;
> val it = fn : Thm.thm -> string
> but there is no Theory.get_name ;-( In the old Isabelle version the
> following worked fine:
> fun string_of_thy thy = ((last_elem (Sign.stamp_names_of (sign_of
> thy)))^".thy"):theory';
> How could that be achieved in Isabelle2009 ?
> Many thanks in advance,
> Walther

More information about the isabelle-dev mailing list