Re: [isabelle] Possible unsoundness in axclass mechanism



> Is this supposed to happen?

Yes.

> I thought declaring an axclass was supposed to be a conservative extension.

It is. You did not prove False outright but you proved False with the proviso

### Pending sort hypotheses: blurg

which Isabelle prints out together with the thm and which is propagated every
time you use that thm.

Tobias





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