Dear Tobias, I think your "sorted_wrt" is almost (modulo "fun" vs. "inductive") my "linked" from the AFP (Efficient_Mergesort).
https://www.isa-afp.org/browser_info/current/AFP/Efficient-Mergesort/Efficient_Sort.html Maybe we could unify the constants/names somehow? At the moment I somewhat prefer "linked" (or maybe "linked_by") since sortedness implies that "P" is some kind of order, which it doesn't have to be. kind regards, chris -------- Forwarded Message -------- Subject: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy Date: Tue, 15 Aug 2017 19:47:08 +0200 From: nipkow <> added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
