[isabelle] lemma on Suc-bounded allquantification



Dear all,

I seem to reprove the following lemma a lot recently (which I then use
as a simp rule):

lemma all_Suc_conv: "(âi<Suc n. P i) â P 0 â (âi<n. P (Suc i))"
  using less_Suc_eq_0_disj by auto

Any chance that it might end up in the Isabelle distribution (at least I
did not find it in Isabelle2016-1)?

cheers

chris




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