[isabelle] schematic variables and assumption



Hello,

I have the following lemma:

lemma "(¬ (∀ x . P x)) ⟹ (∃ x . ¬ P x)"
apply (rule exI)
apply (rule notI)
apply (erule notE)
apply (rule allI)
apply assumption

After the the rule "apply (rule allI)" the goal becomes:
⋀x. P ?x ⟹ P x

I do not understand why "apply assumption" fail at this point.
I would expect that ?x is unified with x and the proof succeed.

Best regards,

Viorel Preoteasa





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