From: Tobias Nipkow <email@example.com>
Dear pat_completeness experts,
pat_completeness does not seem to like ~=, eg
lemma exception: "(⋀x y. x ≠ y ⟹ P True) ⟹ P t"
exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML")
This came up in trying to prove (via induction_schema) an induction schema with
two subcases, one with x = y and the other with x ~= y.
Probably pat_completness was not designed to handle this.
Last updated: Dec 08 2021 at 08:24 UTC