Changes

Summary

merged
adapted to "sorted" changes

Changeset 9193:75ddd105c56a by nipkow: merged
Changeset 9192:1579d02fb45a by nipkow: adapted to "sorted" changes
The file was modified	`thys/Automatic_Refinement/Lib/Misc.thy` (diff)
The file was modified	`thys/Binomial-Queues/PQ.thy` (diff)
The file was modified	`thys/CakeML/generated/LemExtraDefs.thy` (diff)
The file was modified	`thys/Coinductive/Coinductive_List.thy` (diff)
The file was modified	`thys/Coinductive/Examples/LList_CCPO_Topology.thy` (diff)
The file was modified	`thys/Containers/RBT_Set2.thy` (diff)
The file was modified	`thys/Containers/RBT_ext.thy` (diff)
The file was modified	`thys/Containers/Set_Impl.thy` (diff)
The file was modified	`thys/Containers/Set_Linorder.thy` (diff)
The file was modified	`thys/Efficient-Mergesort/Efficient_Sort.thy` (diff)
The file was modified	`thys/Formula_Derivatives/Abstract_Formula.thy` (diff)
The file was modified	`thys/Imperative_Insertion_Sort/Imperative_Insertion_Sort.thy` (diff)
The file was modified	`thys/KBPs/List_local.thy` (diff)
The file was modified	`thys/KBPs/ODList.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Auxiliary/List2.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Impl/Mojmir_Rabin_Impl.thy` (diff)
The file was modified	`thys/Landau_Symbols/Group_Sort.thy` (diff)
The file was modified	`thys/Landau_Symbols/Landau_Real_Products.thy` (diff)
The file was modified	`thys/List-Index/List_Index.thy` (diff)
The file was modified	`thys/List-Infinite/ListInf/List2.thy` (diff)
The file was modified	`thys/List_Update/List_Factoring.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/Init_Normalization.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/List_More.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/Pi_Regular_Exp.thy` (diff)
The file was modified	`thys/Matrix/Utility.thy` (diff)
The file was modified	`thys/Median_Of_Medians_Selection/Median_Of_Medians_Selection.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Missing_List.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Prime_Factorization.thy` (diff)
The file was modified	`thys/Polynomials/MPoly_Type_Class.thy` (diff)
The file was modified	`thys/Polynomials/Polynomials.thy` (diff)
The file was modified	`thys/Polynomials/Utils.thy` (diff)
The file was modified	`thys/Selection_Heap_Sort/RemoveMax.thy` (diff)
The file was modified	`thys/Splay_Tree/Splay_Tree.thy` (diff)