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



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.


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