[isabelle-dev] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy

[Christian Sternagel]

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