Re: [isabelle] Problem with unfolding definitions while instantiating class



On 09/06/2014 11:24, Florian Haftmann wrote:
>> This is not possible. As Dave pointed out, the problem goes away if in
>> Main the instantiation of "fun" on class complete_lattice is done in
>> stages, where in a first step one merely instantiates Sup and Inf.
>> 
>> @ Florian: any objections to that?
> 
> No.  This would finally conclude the »syntactification« of Sup and Inf 
> initiated by Larry (AFAIR).

It is in now. This means that with the next release one can use Inf and Sup on
functions without forcing things to be complete lattices.

Tobias




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