*To*: Rob Arthan <rda at lemma-one.com>*Subject*: Re: [isabelle] Definition in (and of) Isabelle/HOL*From*: Makarius <makarius at sketis.net>*Date*: Fri, 11 Apr 2014 13:34:40 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <A6F928CE-9C6D-4248-B9E8-D8B2706EBB05@lemma-one.com>*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>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 11 Apr 2014, Rob Arthan wrote:

This is addressed in HOL Light along the following lines: it defines afunction on the natural numbers such that 1 < x(n) < 10 for all n, andthen defines c = x(42) and d = x(43), assuming that c is the 42ndconstant that HOL Light has been asked to define.

Makarius

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

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

- Previous by Date: Re: [isabelle] Definition in (and of) Isabelle/HOL
- Next by Date: Re: [isabelle] system of representatives of an equivalence relation
- 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