*To*: Michael Norrish <Michael.Norrish at nicta.com.au>*Subject*: Re: [isabelle] referring to constants that have just been defined*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Tue, 28 Mar 2006 08:51:10 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <17448.35100.167623.309679@raceme.rsise.anu.edu.au>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <17447.11821.999387.65218@raceme.rsise.anu.edu.au> <442790C1.6030207@informatik.tu-muenchen.de> <17448.35100.167623.309679@raceme.rsise.anu.edu.au>*User-agent*: Thunderbird 1.5 (X11/20060113)

> 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.

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

**References**:**[isabelle] referring to constants that have just been defined***From:*Michael Norrish

**Re: [isabelle] referring to constants that have just been defined***From:*Florian Haftmann

**Re: [isabelle] referring to constants that have just been defined***From:*Michael Norrish

- Previous by Date: Re: [isabelle] referring to constants that have just been defined
- Next by Date: [isabelle] short-cut for defining inductive relations
- Previous by Thread: Re: [isabelle] referring to constants that have just been defined
- Next by Thread: [isabelle] Featherweight Java formalization in Isabelle?
- Cl-isabelle-users March 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list