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
Isabelle/db8f94656024.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
