Summary
- re-established AFP entry for FinFuns as library
- clarified comment
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Library/Library.thy (diff) |
The file was modified | src/HOL/ROOT (diff) |
The file was removed | src/HOL/Library/FinFun.thy |
The file was removed | src/HOL/ex/FinFunPred.thy |
The file was modified | src/HOL/Tools/Nitpick/nitpick_hol.ML (diff) |