Re: [isabelle] Possible unsoundness in axclass mechanism

> Is this supposed to happen?


> 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.


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