Quoting Tjark Weber <[email protected]>:
Well, "roundup bound" is developer jargon.
Yes, but this is just because the roundup algorithm hasn't been documented anywhere.
If you have a permutation of more than five parameters, you might need to increase the bound (but I consider this very unlikely, so you would need to recompile Isabelle for the change). Likewise if you have a very long cyclic dependency.
"Sublocale relation probably not terminating" points into the right direction, but is not very precise (because cyclic sublocale relations are, in general, permitted).
I agree that the error message should be more explicit about that the problem is that the attempted sublocale declaration is not feasible in some sense.
Clemens _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
