Summary
- merged
- move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
- superfluous premise (noticed by Julian Nagele)
The file was added | src/HOL/Library/Complete_Partial_Order2.thy |
The file was modified | CONTRIBUTORS (diff) |
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Library/Library.thy (diff) |
The file was modified | src/HOL/Library/Multiset.thy (diff) |
The file was modified | src/HOL/ZF/LProd.thy (diff) |