[isabelle-dev] Local Specification Mechanisms: Brief Experience Report

[Clemens Ballarin]

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  
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