[isabelle-dev] Incoherent use of file name "hoare_syntax.ML"
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
> 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
Moreover, I have brushed up the HOL-Hoare session document in
More information about the isabelle-dev