[isabelle-dev] finite_intvl_succ

[Tobias Nipkow]

Intentionally. The main purpose of that class is to provide the list 
interval notation [_.._]. For nat there is already [_..<_] with lots of 
lemmas. Having both intervals on nat will require lots of bridging lemmas.

Tobias

Amine Chaieb wrote:
> This is a nice generalization for intervals, but on main candidate was 
> missing for instantiation : natural number!
> 
> Amine.
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev