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