[isabelle-dev] finite_intvl_succ

Tobias Nipkow nipkow at in.tum.de
Mon Jan 28 08:03:57 CET 2008

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.


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

More information about the isabelle-dev mailing list