Re: [isabelle] lemma on Suc-bounded allquantification

All_less_Suc is in the distribution:

 - Johannes

On Tue, 2017-08-08 at 12:37 +0200, Christian Sternagel wrote:
> 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.