[isabelle-dev] Incoherent use of file name "hoare_syntax.ML"

Makarius makarius at sketis.net
Wed Dec 23 15:56:35 CET 2020

On 23/12/2020 10:08, Lars Hupel wrote:
> Based on my superficial understanding, this problem appears to be caused by
> two different theories including the same ML file
> (src/HOL/Hoare/hoare_syntax.ML).

There is something conceptually wrong here. I will see how to get it right.

> Since the ML file is dependent on syntax that is independently introduced by
> those theories, I'm unsure how to fix this. The naive solution would be to
> duplicate the ML file, but that seems inelegant.

Duplication is even worse.


More information about the isabelle-dev mailing list