--- a/NEWS Sun Aug 10 23:30:55 2025 +0200
+++ b/NEWS Sun Aug 10 23:32:06 2025 +0200
@@ -335,6 +335,19 @@
*** System ***
+* The command-line tool "isabelle process_theories" tool takes source
+files and theories within a proper session context (like regular
+"isabelle build"). Output of prover messages works roughly like
+"isabelle build_log", while the theories are being processed.
+
+Examples:
+
+ isabelle process_theories -O HOL-Library.Multiset
+
+ isabelle process_theories -O -o show_states HOL-Library.Multiset
+
+ isabelle process_theories -f '~~/src/HOL/Examples/Seq.thy'
+
* System option "show_results" (default true) controls output of
toplevel command results (definitions, theorems) in batch-builds. In
interactive mode this is always enabled; in batch-builds it can be