# HG changeset patch
# User Kevin Kappelmann <kevin.kappelmann@tum.de>
# Date 1742757876 -3600
#      Sun Mar 23 20:24:36 2025 +0100
# Node ID b336fcbd142d2dd8b04ab4eb4f67620bd8392ba0
# Parent  a66e8d921c718cd38a1d81d416256cd95344feff
feat(ML_Unification/priorities) add doubling of prios

diff --git a/thys/ML_Unification/ML_Utils/Priorities/priority.ML b/thys/ML_Unification/ML_Utils/Priorities/priority.ML
--- a/thys/ML_Unification/ML_Utils/Priorities/priority.ML
+++ b/thys/ML_Unification/ML_Utils/Priorities/priority.ML
@@ -16,6 +16,7 @@
 
   val between : prio * prio -> prio
   val halve : prio -> prio
+  val double : prio -> prio
 
   val inc : prio -> prio
   val dec : prio -> prio
@@ -51,6 +52,7 @@
 
 fun between (p1, p2) = Prio ((dest_prio p1 + dest_prio p2) / two_rat)
 fun halve p = between (BOTTOM_EXCLUSIVE, p)
+fun double p = Prio (dest_prio p * two_rat) (*assumption: BOTTOM_EXCLUSIVE = 0*)
 
 val epsilon = Rat.make (1, 100)
 fun inc p = Prio (dest_prio p + epsilon)
@@ -78,4 +80,4 @@
       >> prio_from_code)
   end
 
-end
\ No newline at end of file
+end