Summary
- more operations for lexicographic ordering;
- more operations: following Library list operations and Ord_List.T operations;
- tuned;
- tuned;
The file was modified | src/Pure/General/set.ML (diff) |
The file was modified | src/Pure/library.ML (diff) |
The file was modified | src/Pure/General/set.ML (diff) |
The file was modified | src/Pure/library.ML (diff) |
The file was modified | src/Pure/General/set.ML (diff) |