Re: [isabelle] Possible unsoundness in axclass mechanism
On Wednesday 14 September 2005 18:36, Tom Ridge wrote:
> axclass blurg < type
> blurg: "! x. x ~= x"
> lemma "False"
> apply(rule l[of "x"])
> apply(simp only: blurg)
> Is this supposed to happen? I thought declaring an axclass was supposed to
> be a conservative extension.
You should see a warning "### Pending sort hypotheses: blurg" when proving
"False" in the above way, meaning that the lemma only holds under the
assumption that the type class blurg is non-empty. There is a short
discussion of this issue at the end of Section 8.3 of the Isabelle/HOL
This archive was generated by a fusion of
Pipermail (Mailman edition) and