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”

and

	“~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 http://isabelle.in.tum.de/dist/Isabelle2013-2/doc/isar-ref.pdf 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.


	Makarius


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