[isabelle-dev] finite_intvl_succ

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 o

[isabelle-dev] finite_intvl_succ

This is a nice generalization for intervals, but on main candidate was missing for instantiation : natural number! Amine.