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

[Makarius]

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