On 08/01/2021 16:10, Manuel Eberl wrote: > I have a small amount of material for HOL-Data_Structures and for > Algebraic_numbers in the AFP. Will put that in in the next day or two. OK, just tell me when you are finished. Makarius