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
