Re: [isabelle] referring to constants that have just been defined



Hello Michael,

It seems that using
  Sign.intern_const

will give me the correct qualified name for the constant (I do know
its name after all), but I'm worried about the situation when multiple
constants from different theories have the same name.  What will
intern_const do then?

Is there a function that will give me the name of the current theory,
so that I can construct the fully-qualified name myself?

Context.theory_name or Sign.full_name may prove helpful. But be aware that though the default naming policy is indeed "theory name + unqualified name", this might be changed.

Florian

--

PGP available:
http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de.pgp
begin:vcard
fn:Florian Haftmann
n:Haftmann;Florian
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at informatik.tu-muenchen.de
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =
	=0D=0A=
	http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_i=
	nformatik_tu_muenchen_de.pgp=0D=0A=
	
x-mozilla-html:FALSE
url:http://isabelle.in.tum.de/~haftmann
version:2.1
end:vcard



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