I looked into your theory but did not find any further generic lemmas about "linked". Let me know if I missed any that should go into List.
Tobias On 16/08/2017 10:44, Christian Sternagel wrote:
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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev