Re: [isabelle] Definition in (and of) Isabelle/HOL
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and