Re: [isabelle] Lattices and syntactic classes
On 09/08/2011 11:00 PM, Makarius wrote:
A further aspect: Pure.intro declaration have precedence over the intro
classes method, as shown in the folling silly example:
lemma nonsense [Pure.intro]:
"False \<Longrightarrow> OFCLASS('a, default_class)"
instance bool :: default
By declaring your customary class introduction rules Pure.intro, they
are preferred in instance proofs.
Does that solve the issues that were raised on this thread earlier?
To me this looks rather like a workaround for some specific situations.
If I understand correctly, it wouldn't work with a more complex class
hierarchy, where parts of the instance may already be established etc.
The issue certainly deserves more thourough examination at some point.
For now I have just added (5e51075cbd97) the syntactic classes for inf
and sup, which were originally asked for by Viorel. This is a rather
straightforward thing, and the more general typings that may arise seem
to have little impact in practice.
This archive was generated by a fusion of
Pipermail (Mailman edition) and