Changes

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

Changeset 63378:161f3ce4bf45 by haftmann: spelling
The file was modified	`NEWS` (diff)
Changeset 63377:64adf4ba9526 by haftmann: combinator to build partial equivalence relations from a predicate and an equivalenc relation
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)
Changeset 63376:4c0cc2b356f0 by haftmann: default one-step rules for predicates on relations;<br>clarified status of legacy input abbreviations
The file was modified	`src/HOL/Relation.thy` (diff)
Changeset 63375:59803048b0e8 by haftmann: basic facts about almost everywhere fix bijections
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)
Changeset 63374:1a474286f315 by haftmann: dedicated locale for total bijections
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Hilbert_Choice.thy` (diff)
Changeset 63373:487d764fca4a by haftmann: tuned sections
The file was modified	`src/HOL/Binomial.thy` (diff)
Changeset 63372:492b49535094 by haftmann: relating gbinomial and binomial, still using distinct definitions
The file was modified	`src/HOL/Binomial.thy` (diff)