# HG changeset patch # User wenzelm # Date 1540933716 -3600 # Node ID be8c70794375eee3a2b93bb2579fe0859295c8c4 # Parent 7062639cfdaa94fb3eed9b8a69b89df6262e08ca tuned example; diff -r 7062639cfdaa -r be8c70794375 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 \ +ML_command \ GHC.read_source \<^context> \ allConst, impConst, eqConst :: String allConst = \\<^const_name>\Pure.all\\ impConst = \\<^const_name>\Pure.imp\\ eqConst = \\<^const_name>\Pure.eq\\ \ - |> File.write \<^path>\consts.hs\ + |> writeln \