Re: [isabelle] lemma on Suc-bounded allquantification



Dear Johannes,

thanks! So I just have to wait for the next release ;)

What about the equivalent lemma for exists?

cheers

chris

On 08/08/2017 04:38 PM, Johannes HÃlzl wrote:
> 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.