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



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.


	Makarius




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