[isabelle-dev] Local Specification Mechanisms: Brief Experience Report
ballarin at in.tum.de
Fri Dec 17 21:46:48 CET 2010
Quoting Tjark Weber <webertj at in.tum.de>:
> Well, "roundup bound" is developer jargon.
Yes, but this is just because the roundup algorithm hasn't been
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
More information about the isabelle-dev