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
> How could that be achieved in Isabelle2009 ?
> Many thanks in advance,
More information about the isabelle-dev