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

Makarius makarius at sketis.net
Thu Dec 24 00:10:58 CET 2020

On 23/12/2020 15:56, Makarius wrote:
> 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.

I have reworked it in Isabelle/b1be35908165, to make it fit better into
contemporary Isabelle.

Moreover, I have brushed up the HOL-Hoare session document in


More information about the isabelle-dev mailing list