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
That is a refurbished version of really ancient explanations by Larry, but
this material is still interesting, and should be up-to-date concerning
This archive was generated by a fusion of
Pipermail (Mailman edition) and