Summary
- merged
- more "sorted" changes
- more "sorted" changes
- new def of sorted and sorted_wrt
The file was modified | src/HOL/List.thy (diff) |
The file was modified | src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy (diff) |
The file was modified | src/HOL/Imperative_HOL/ex/Sorted_List.thy (diff) |
The file was modified | src/HOL/Data_Structures/Binomial_Heap.thy (diff) |
The file was modified | src/HOL/Data_Structures/Sorted_Less.thy (diff) |
The file was modified | src/HOL/Data_Structures/Tree234_Set.thy (diff) |
The file was modified | src/HOL/Data_Structures/Tree23_Set.thy (diff) |
The file was modified | src/HOL/Library/RBT_Impl.thy (diff) |
The file was modified | src/HOL/Library/RBT_Set.thy (diff) |
The file was modified | src/HOL/Library/Tree.thy (diff) |
The file was modified | src/HOL/List.thy (diff) |
The file was modified | src/HOL/ex/Bubblesort.thy (diff) |
The file was modified | src/HOL/ex/MergeSort.thy (diff) |
The file was modified | src/HOL/ex/Quicksort.thy (diff) |