Re: [isabelle] lemma on Suc-bounded allquantification
thanks! So I just have to wait for the next release ;)
What about the equivalent lemma for exists?
On 08/08/2017 04:38 PM, Johannes HÃlzl wrote:
> 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
>> 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)?
This archive was generated by a fusion of
Pipermail (Mailman edition) and