[isabelle] How to delete rules applied by clarify
lemma "~ a \<subseteq> b ==> P"
I get the subgoal
!!x. [|~P; x:a|] ==> x:b
However, I cannot find any rule in the claset (print_claset) that seems
to be responsible for this transformation.
A deeper inspection reveals that there is the rule
"¬ A1 ⊆ B1 ⟹ (⋀x. ¬ R ⟹ x ∈ A1 ⟹ x ∈ B1) ⟹ R"
in the "safep_netpair" - component of the claset. (which is not printed
Moreover, there seems to be no way to get the rule out there. A
[rule del] just sais "undeclared classical rule".
So what is going on here, and, more important:
How to stop clarify from doing this transformation, and leaving the
original conclusion of the subgoal intact?
This archive was generated by a fusion of
Pipermail (Mailman edition) and