# HG changeset patch
# User wenzelm
# Date 1487935453 -3600
# Node ID b69ef432438dfe6ccf93170a587a743dd69b45d6
# Parent  0940a741adf7c2b97ed125ff4b8895c08cf487a8
avoid Unicode that conflicts with Isabelle symbol rendering;

diff -r 0940a741adf7 -r b69ef432438d NEWS
--- a/NEWS	Wed Feb 22 21:12:23 2017 +0100
+++ b/NEWS	Fri Feb 24 12:24:13 2017 +0100
@@ -16,9 +16,9 @@
 directly into ML, alongside with @{code} antiquotations, using
 the following antiquotations:
 
-  @{computation … terms: … datatypes: …} : ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
-  @{computation_conv … terms: … datatypes: …} : (Proof.context -> 'ml -> conv) -> Proof.context -> conv
-  @{computation_check terms: … datatypes: …} : Proof.context -> conv
+  @{computation ... terms: ... datatypes: ...} : ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
+  @{computation_conv ... terms: ... datatypes: ...} : (Proof.context -> 'ml -> conv) -> Proof.context -> conv
+  @{computation_check terms: ... datatypes: ...} : Proof.context -> conv
 
 See src/HOL/ex/Computations.thy, src/HOL/Decision_Procs/Commutative_Ring.thy
 and src/HOL/Decision_Procs/Reflective_Field.thy for examples and