NEWS
changeset 78528 3d6dbf215559
parent 78526 fd3fa1790a96
child 78587 12aac1489f3b
--- a/NEWS	Sun Aug 13 19:23:53 2023 +0200
+++ b/NEWS	Sun Aug 13 19:27:58 2023 +0200
@@ -423,11 +423,10 @@
   isabelle process -l ZF -e "Session.print_context_tracing (K true)"
 
 An alternative to "isabelle process -l ZF" is "isabelle jedit -l ZF"
-with with the Isar command 'print_context_tracing' or with the
-subsequent ML snippets (in an arbitrary theory context):
-
-  ML_command \<open>Session.print_context_tracing (K true)\<close>
-  ML \<open>Context.finish_tracing ()\<close>
+with the subsequent Isar commands:
+
+  print_context_tracing
+  print_context_tracing ZF.Nat ZF.Int  \<comment> \<open>restriction to theories\<close>
 
 * The "rsync" tool has been bundled as Isabelle component, with uniform
 version and compilation options on all platforms. This allows to use