Re: [isabelle] Isabelle help



Hi,

 theorem 211: "(l \<noteq> m) \<Longrightarrow> ((\<exists>P. (incident
 l P \<and> incident m P)) \<or> \<not>(\<exists>P. (incident l P
 \<and> incident m P)))"

by blast


Amine.





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