[isabelle-dev] Pending sort hypotheses

On Thu, 2 Jul 2009, Amine Chaieb wrote: > Many thanks for the explanation. Indeed, if I make Abstract_Rat import > say Complex_Main, the proofs work without the sort assumption. This must > be due to the fact that concrete instances of field (I think) come only > after Main. The proofs in Abstrac

[isabelle-dev] NEWS

* Changed DERIV_intros to a NamedThmsFun. Each of the theorems in DERIV_intros assumes composition with an additional function and matches a variable to the derivative, which has to be solved by the simplifier. Hence (auto intro!: DERIV_intros) computes the derivative of most elementary terms. * M

[isabelle-dev] Pending sort hypotheses

Hi Brian, Many thanks for the explanation. Indeed, if I make Abstract_Rat import say Complex_Main, the proofs work without the sort assumption. This must be due to the fact that concrete instances of field (I think) come only after Main. > That's exactly right. Theorems need to have sort hypothe