I would be OK with / for integer division, but there would be a lot of 
compatibility issues.
Larry

> On 2 Jun 2015, at 19:17, Florian Haftmann 
> <florian.haftm...@informatik.tu-muenchen.de> wrote:
> 
> a) The radical solution: there is only »_ / _« for both field division
> and euclidean division. How natural is notation like »a / b * b + a mod
> b = a« then?

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to