Re: [isabelle] lemma on Suc-bounded allquantification



All_less_Suc is in the distribution:

  http://isabelle.in.tum.de/repos/isabelle/rev/e44f5c123f26

Best,
 - 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.