Email Gateway (Nov 03 2020 at 12:50): Email Gateway (Nov 03 2020 at 12:50):From: Tobias Nipkow <nipkow@in.tum.de>
Dear pat_completeness experts,
pat_completeness does not seem to like ~=, eg
lemma exception: "(⋀x y. x ≠ y ⟹ P True) ⟹ P t"
apply(pat_completeness)
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.
Tobias
smime.p7s
Last updated: Jan 04 2025 at 20:18 UTC