*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Definition in (and of) Isabelle/HOL*From*: Rob Arthan <rda at lemma-one.com>*Date*: Fri, 11 Apr 2014 14:24:31 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1404111331160.6339@lxbroy10.informatik.tu-muenchen.de>*References*: <4D708E4D-27BA-4AF8-A2E3-54C2A9DCECBB@lemma-one.com> <alpine.LNX.2.00.1403311637260.15927@lxbroy10.informatik.tu-muenchen.de> <A6F928CE-9C6D-4248-B9E8-D8B2706EBB05@lemma-one.com> <alpine.LNX.2.00.1404111331160.6339@lxbroy10.informatik.tu-muenchen.de>

Makarius, On 11 Apr 2014, at 12:34, Makarius <makarius at sketis.net> wrote: > On Fri, 11 Apr 2014, Rob Arthan wrote: > >> This is addressed in HOL Light along the following lines: it defines a function on the natural numbers such that 1 < x(n) < 10 for all n, and then defines c = x(42) and d = x(43), assuming that c is the 42nd constant that HOL Light has been asked to define. > > Another observation about this detail: this approach of HOL Light assumes a single linear theort context. In Isabelle we've had a DAG of theories (with merge), ever since Larry introduced that in 1989. One could still do a similar trick there, but with more structure for these intro-logical indentifiers. Good point! This trick wouldn’t work properly in HOL4 or ProofPower for exactly the same reason. Regards, Rob.

**References**:**Re: [isabelle] Definition in (and of) Isabelle/HOL***From:*Rob Arthan

**Re: [isabelle] Definition in (and of) Isabelle/HOL***From:*Makarius

- Previous by Date: Re: [isabelle] system of representatives of an equivalence relation
- Next by Date: Re: [isabelle] Default implementations for instances
- Previous by Thread: Re: [isabelle] Definition in (and of) Isabelle/HOL
- Next by Thread: Re: [isabelle] Definition in (and of) Isabelle/HOL
- Cl-isabelle-users April 2014 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