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



> In particular, what does intern_const do when there are multiple
> constants of the same name in different theories?

theory Scratch
imports Main
begin

consts
  map :: unit

ML {*
Sign.intern_const (the_context ()) "map"
*}

	>>> Scratch.map

ML {*
Sign.extern_const (the_context ()) "List.map"
*}

	>>> List.map

ML {*
Sign.extern_const (the_context ()) "Scratch.map"
*}

	>>> Scratch.map

Thanks for that.  So it does seem as if I should use
Sign.intern_const.

In this context, this should work. But the naming policy is a very flexible mechanism that might be changed (though this is rarely done in practice).

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.