[isabelle-dev] Error in "cite" anitquotation

[Makarius]

On 21/01/2023 20:24, Lawrence Paulson wrote:
> I used the one in Types_Tableaus_and_Goedels_God with some modifications and 
> one entry of my own. Seems to work.
> 
> For the future, do we need to prohibit entries with explicit bibliographies?

It would indeed be better to standardize everything towards proper root.bib + 
regular bibtex setup (which is implicit in the document build process).

We have very few exceptions so far, it should be easy to upgrade them.

That is mainly a matter to search for unchecked \cite or \bibitem commands, 
but we also need proper bibtex entries from somewhere.


	Makarius