Summary
- added inj_def (redundant, analogous to surj_def, bij_def); tuned proofs;
- tuned proofs;
- tuned proof;
- tuned whitespace;
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) |
The file was modified | src/HOL/Fun.thy (diff) |
The file was modified | src/HOL/Power.thy (diff) |
The file was modified | src/HOL/List.thy (diff) |