diff -r 8f0b2daa7eaa -r d93ead9ac6df NEWS --- 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