Am 30/05/2013 13:41, schrieb Lawrence Paulson: > The only question is whether Isabelle is important enough for such work to be seen as significant in a wider context. Makarius is right, the interaction of schematic type variables and HOU has never been nailed down properly and would be of interest to a larger community. Tobias