Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. added inj_def (redundant, analogous to surj_def, bij_def); tuned proofs;
  2. tuned proofs;
  3. tuned proof;
  4. tuned whitespace;
Changeset 64966:d53d7ca3303e by wenzelm:
added inj_def (redundant, analogous to surj_def, bij_def);<br>tuned proofs;
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Fun.thy (diff)
The file was modified src/HOL/Library/Indicator_Function.thy (diff)
The file was modified src/HOL/Library/Permutations.thy (diff)
The file was modified src/HOL/List.thy (diff)
Changeset 64965:d55d743c45a2 by wenzelm:
tuned proofs;
The file was modified src/HOL/Fun.thy (diff)
Changeset 64964:a0c985a57f7e by wenzelm:
tuned proof;
The file was modified src/HOL/Power.thy (diff)
Changeset 64963:fc4d1ceb8e29 by wenzelm:
tuned whitespace;
The file was modified src/HOL/List.thy (diff)