Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. remove typo in bij_swap_compose_bij theorem name; tune proof
  2. filter non-matching prems to not fail in proof procedure; include test case (related to c8a93680b80d)
Changeset 64543:6b13586ef1a2 by bulwahn:
remove typo in bij_swap_compose_bij theorem name; tune proof
The file was modified NEWS (diff)
The file was modified src/HOL/Library/Permutations.thy (diff)
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)