PRELIMINARY / DO NOT MERGE: adapt to Isabelle_25-Jul-2026 (Isabelle2026 pre-release)

[lawrencecpaulson]

Warning

PRELIMINARY — DO NOT MERGE.
This is opened as a draft to record the precise change set now. It targets the
Isabelle_25-Jul-2026 pre-release, not a released Isabelle. Further
Isabelle2026 pre-releases are expected, so this will need re-checking against
each of them, and it should not land until the transition to Isabelle2026 proper.

What this is

The set of source changes required to build AutoCorrode under the current
Isabelle2026 pre-release. It applies cleanly to main — none of the 25 touched
files have changed upstream since the snapshot this was developed against.

Changes, by cause

ML simplifier API (Crush/{crush,base,seplog}.ML, Misc/*, Autogen/AutoLocality.thy,
Byte_Level_Encoding/*)

• the addsimps / delsimps / addsimprocs / delsimprocs infixes are discontinued
• clear_simpset, simpset_map, merge_ss and the proc_kind constructors are now
  qualified under Simplifier
• Raw_Simplifier.map_ss → Simplifier.map_simpset
• Simplifier.add_proc takes a single simproc, so simproc lists need a fold

Specification (Autogen/AutoLens.thy, Enum_Theory/enum_cmd.ML, Misc/*,
Shallow_Micro_Rust/Simple_Word_Enum_uRust.thy)

• the trailing interactive-mode flag moved into a leading record argument:
  definition / definition_cmd take {verbose}, theorems_cmd takes {verbose, kind}

Isar / toplevel (Shallow_Micro_Rust/Micro_Rust_Shallow_Embedding.thy, ir/ir.ML,
iq/Isar_Explore.thy)

• Outer_Syntax.local_theory' was removed along with the flag it supplied
• Toplevel.command_exception lost its bool argument
• interactive mode and parallel_proofs moved from the Printer / Multithreading
  refs into the new Interactive structure
• OS.Process.sleep is no longer exposed to user-space ML → Time.sleep
• Thy_Info.use_theories takes an Options.update per import instead of one
  global Options.T. Ir.load_theory therefore sets record_theories for the
  requested theory only; its ancestors keep whatever the heap was built with.
  This is a small behavioural narrowing and is the one change here worth a second
  opinion.
• Name_Space.markup → Name_Space.markups, returning a Markup.T list

HOL (Micro_Rust_Examples/Linked_List_Executable_{Hybrid,Physical_Memory}.thy,
Misc/Case_for_Typedefs.thy)

• the list constant enumerate was renamed indexed_from, with the corresponding
  lemma renames

I/Q jEdit plugin (iq/src/*.scala)

• PIDE.editor is gone; JEdit_Editor is now a top-level object
• PIDE.options is the resolved Options, no longer JEdit_Options (drop .value)
• Output_Area, current_node_snapshot, current_command and Hyperlink.follow
  take a JEdit_Editor.Context instead of a bare View
• Document_Status.Node_Status.command_timings is keyed by command id, not
  Command; resolved via Snapshot.get_command
• Rendering is now abstract (it needs a gui_style). JEdit_Rendering accepts any
  Document_Model, so it also covers the former File_Model fallback.
• Scala 3.3.8 with -Werror additionally rejects some latent unused imports,
  parameters and default arguments (note: _-prefixing does not suppress this;
  @scala.annotation.unused does)

Build glue (iq/Makefile, ic2/Makefile, isabelle-assistant/Makefile)

• stop hardcoding the Isabelle version and the contrib Scala version
• for review: the ISABELLE_VERSION default now names the pre-release. That
  will want changing to Isabelle2026 when it is released.

How it was checked

• the AutoCorrode session builds
• the full downstream NICE proof stack builds against it, and its theories were
  additionally checked interactively

Not checked: the ic2 Scala component and the isabelle-assistant plugin were not
compiled, only their Makefiles adjusted. Isabelle/Scala's move to Explicit Nulls and
the new Logger arguments may yet affect them.