Changes

Summary

filter non-matching prems to not fail in proof procedure; include test case (related to c8a93680b80d)

Changeset 64542:c7d76708379f by bulwahn: filter non-matching prems to not fail in proof procedure; include test case (related to c8a93680b80d)
The file was modified	`src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML` (diff)