Re: [isabelle] How to delete rules applied by clarify

On Mon, 14 Apr 2014, Lawrence Paulson wrote:

The point is that logically there is no difference between

	"~ a \<subseteq> b ==> P”


	“~P ==> a \<subseteq> b”.

The classical reasoner is designed to do the same thing in both cases.

More on the design of the classical reasoner is available in section 9.4.

That is a refurbished version of really ancient explanations by Larry, but this material is still interesting, and should be up-to-date concerning current Isabelle.


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