--- 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>