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

Lars Hupel lars at hupel.info
Tue Dec 29 16:44:46 CET 2020


> 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.

This fixed it for Hoare, but we have another problem:

10:01:16 *** Incoherent use of file name 
"$ISABELLE_HOME/src/Doc/antiquote_setup.ML" as 
"files/ISABELLE_HOME/src/Doc/antiquote_setup.ML.html" in theory 
Isabelle_Meta_Model.Generator_static vs. Isabelle_Meta_Model.Design_deep


More information about the isabelle-dev mailing list