tuned example;
authorwenzelm
Tue, 30 Oct 2018 22:08:36 +0100
changeset 69212 be8c70794375
parent 69211 7062639cfdaa
child 69213 ab98f058f9dc
tuned example;
NEWS
--- a/NEWS	Tue Oct 30 22:05:30 2018 +0100
+++ b/NEWS	Tue Oct 30 22:08:36 2018 +0100
@@ -93,14 +93,14 @@
 Haskell string literal. This allows to refer to Isabelle items robustly,
 e.g. via Isabelle/ML antiquotations or library operations. For example:
 
-ML \<open>
+ML_command \<open>
   GHC.read_source \<^context> \<open>
     allConst, impConst, eqConst :: String
     allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
     impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
     eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
   \<close>
-  |> File.write \<^path>\<open>consts.hs\<close>
+  |> writeln
 \<close>