tuned whitespace;
authorwenzelm
Sun Feb 26 23:50:19 2017 +0100 (2017-02-26)
changeset 6505512189e86c49d
parent 65054 9ad3f65c03f4
child 65056 002b4c8c366e
tuned whitespace;
NEWS
     1.1 --- a/NEWS	Sun Feb 26 22:41:10 2017 +0100
     1.2 +++ b/NEWS	Sun Feb 26 23:50:19 2017 +0100
     1.3 @@ -12,17 +12,20 @@
     1.4  * Document antiquotations @{prf} and @{full_prf} output proof terms
     1.5  (again) in the same way as commands 'prf' and 'full_prf'.
     1.6  
     1.7 -* Computations generated by the code generator can be embedded
     1.8 -directly into ML, alongside with @{code} antiquotations, using
     1.9 -the following antiquotations:
    1.10 -
    1.11 -  @{computation ... terms: ... datatypes: ...} : ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
    1.12 -  @{computation_conv ... terms: ... datatypes: ...} : (Proof.context -> 'ml -> conv) -> Proof.context -> conv
    1.13 +* Computations generated by the code generator can be embedded directly
    1.14 +into ML, alongside with @{code} antiquotations, using the following
    1.15 +antiquotations:
    1.16 +
    1.17 +  @{computation ... terms: ... datatypes: ...} :
    1.18 +    ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
    1.19 +  @{computation_conv ... terms: ... datatypes: ...} :
    1.20 +    (Proof.context -> 'ml -> conv) -> Proof.context -> conv
    1.21    @{computation_check terms: ... datatypes: ...} : Proof.context -> conv
    1.22  
    1.23 -See src/HOL/ex/Computations.thy, src/HOL/Decision_Procs/Commutative_Ring.thy
    1.24 -and src/HOL/Decision_Procs/Reflective_Field.thy for examples and
    1.25 -the tutorial on code generation.
    1.26 +See src/HOL/ex/Computations.thy,
    1.27 +src/HOL/Decision_Procs/Commutative_Ring.thy and
    1.28 +src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
    1.29 +tutorial on code generation.
    1.30  
    1.31  
    1.32  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.33 @@ -108,13 +111,14 @@
    1.34  * The theorem in Permutations has been renamed:
    1.35    bij_swap_ompose_bij ~> bij_swap_compose_bij
    1.36  
    1.37 -* Session HOL-Library: The simprocs on subsets operators of multisets have been renamed:
    1.38 +* Session HOL-Library: The simprocs on subsets operators of multisets
    1.39 +have been renamed:
    1.40    msetless_cancel_numerals ~> msetsubset_cancel
    1.41    msetle_cancel_numerals ~> msetsubset_eq_cancel
    1.42  INCOMPATIBILITY.
    1.43  
    1.44 -* Session HOL-Library: The suffix _numerals has been removed from the name of the simprocs on multisets.
    1.45 -INCOMPATIBILITY.
    1.46 +* Session HOL-Library: The suffix _numerals has been removed from the
    1.47 +name of the simprocs on multisets. INCOMPATIBILITY.
    1.48  
    1.49  
    1.50  *** System ***