Summary
- spelling
- combinator to build partial equivalence relations from a predicate and an equivalenc relation
- default one-step rules for predicates on relations; clarified status of legacy input abbreviations
- basic facts about almost everywhere fix bijections
- dedicated locale for total bijections
- tuned sections
- relating gbinomial and binomial, still using distinct definitions
The file was modified | NEWS (diff) |
The file was added | src/HOL/Library/Combine_PER.thy |
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Library/Library.thy (diff) |
The file was modified | src/HOL/Relation.thy (diff) |
The file was added | src/HOL/Library/Perm.thy |
The file was added | src/HOL/ex/Perm_Fragments.thy |
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Library/Dlist.thy (diff) |
The file was modified | src/HOL/Library/Library.thy (diff) |
The file was modified | src/HOL/ROOT (diff) |
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Hilbert_Choice.thy (diff) |
The file was modified | src/HOL/Binomial.thy (diff) |
The file was modified | src/HOL/Binomial.thy (diff) |