# Re: [isabelle] Possible unsoundness in axclass mechanism

Hi Tom,
> theory False = Main:
>
> axclass blurg < type
> blurg: "! x. x ~= x"
>
> lemma l: "(x ~= (x::'a::blurg)) ==> False"
> apply(simp)
> done
>
> lemma "False"
> apply(rule l[of "x"])
> apply(simp only: blurg)
> apply(simp)
> done
When finishing the questionable theorem you get the message
### Pending sort hypotheses: blurg
Sort hypotheses are additional hypotheses which state that certain type classes
must be consistent for the theorem to hold. So what you proved is actually "If
there is a type satisfying axiom blurg, then False".
Sort hypotheses are tracked by the system and are usually automatically resolved
my making use of proven instances for the axclasses. If there is no such
instance, this fails and you get the above warning.
You can get a list of unsolved sort hypotheses of a theorem by
ML {* extra_shyps (thm "thm_name") *}
So, what was your instance for "blurg" again?
Alex

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