avoid Unicode that conflicts with Isabelle symbol rendering;
authorwenzelm
Fri Feb 24 12:24:13 2017 +0100 (2017-02-24)
changeset 65045b69ef432438d
parent 65044 0940a741adf7
child 65046 18f3d341f8c0
avoid Unicode that conflicts with Isabelle symbol rendering;
NEWS
     1.1 --- a/NEWS	Wed Feb 22 21:12:23 2017 +0100
     1.2 +++ b/NEWS	Fri Feb 24 12:24:13 2017 +0100
     1.3 @@ -16,9 +16,9 @@
     1.4  directly into ML, alongside with @{code} antiquotations, using
     1.5  the following antiquotations:
     1.6  
     1.7 -  @{computation … terms: … datatypes: …} : ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
     1.8 -  @{computation_conv … terms: … datatypes: …} : (Proof.context -> 'ml -> conv) -> Proof.context -> conv
     1.9 -  @{computation_check terms: … datatypes: …} : Proof.context -> conv
    1.10 +  @{computation ... terms: ... datatypes: ...} : ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
    1.11 +  @{computation_conv ... terms: ... datatypes: ...} : (Proof.context -> 'ml -> conv) -> Proof.context -> conv
    1.12 +  @{computation_check terms: ... datatypes: ...} : Proof.context -> conv
    1.13  
    1.14  See src/HOL/ex/Computations.thy, src/HOL/Decision_Procs/Commutative_Ring.thy
    1.15  and src/HOL/Decision_Procs/Reflective_Field.thy for examples and