NEWS
changeset 82695 d93ead9ac6df
parent 82692 8f0b2daa7eaa
child 82699 a3e7732b0393
--- a/NEWS	Thu Jun 12 08:03:05 2025 +0200
+++ b/NEWS	Thu Jun 12 12:44:47 2025 +0200
@@ -279,6 +279,21 @@
 etc.
 
 
+*** ML ***
+
+* Some old infix operations have been removed. INCOMPATIBILITY. The
+subsequent replacements have slightly different syntactic precedence and
+may require change of parentheses:
+
+  setloop       |> Simplifier.set_loop
+  addloop       |> Simplifier.add_loop
+  delloop       |> Simplifier.del_loop
+  setSSolver    |> Simplifier.set_safe_solver
+  addSSolver    |> Simplifier.add_safe_solver
+  setSolver     |> Simplifier.set_unsafe_solver
+  addSolver     |> Simplifier.add_unsafe_solver
+
+
 *** System ***
 
 * System option "record_theories" tells "isabelle build" to record