>(FWIW) Gemini agrees

LLM hallucination: Poly/ML has been in use since at least 1986 (see e.g. Paulsons preliminary user's manual for Isabelle).