tuned;
authorwenzelm
Sat Sep 09 16:51:55 2017 +0200 (21 months ago)
changeset 6666349318345c332
parent 66650 bcea02893d17
child 66664 91fc9816a86f
tuned;
src/Doc/Implementation/ML.thy
src/Doc/Implementation/Proof.thy
     1.1 --- a/src/Doc/Implementation/ML.thy	Fri Sep 08 19:55:18 2017 +0200
     1.2 +++ b/src/Doc/Implementation/ML.thy	Sat Sep 09 16:51:55 2017 +0200
     1.3 @@ -946,9 +946,9 @@
     1.4    Another benefit of @{ML add_content} is its ``open'' form as a function on
     1.5    buffers that can be continued in further linear transformations, folding
     1.6    etc. Thus it is more compositional than the naive @{ML slow_content}. As
     1.7 -  realistic example, compare the old-style @{ML "Term.maxidx_of_term: term ->
     1.8 -  int"} with the newer @{ML "Term.maxidx_term: term -> int -> int"} in
     1.9 -  Isabelle/Pure.
    1.10 +  realistic example, compare the old-style
    1.11 +  @{ML "Term.maxidx_of_term: term -> int"} with the newer @{ML
    1.12 +  "Term.maxidx_term: term -> int -> int"} in Isabelle/Pure.
    1.13  
    1.14    Note that @{ML fast_content} above is only defined as example. In many
    1.15    practical situations, it is customary to provide the incremental @{ML
    1.16 @@ -1851,18 +1851,18 @@
    1.17    evaluation via promises, evaluation with time limit etc.
    1.18  
    1.19    \<^medskip>
    1.20 -  An \<^emph>\<open>unevaluated expression\<close> is represented either as unit abstraction \<^verbatim>\<open>fn
    1.21 -  () => a\<close> of type \<^verbatim>\<open>unit -> 'a\<close> or as regular function \<^verbatim>\<open>fn a => b\<close> of type
    1.22 -  \<^verbatim>\<open>'a -> 'b\<close>. Both forms occur routinely, and special care is required to
    1.23 -  tell them apart --- the static type-system of SML is only of limited help
    1.24 +  An \<^emph>\<open>unevaluated expression\<close> is represented either as unit abstraction
    1.25 +  \<^verbatim>\<open>fn () => a\<close> of type \<^verbatim>\<open>unit -> 'a\<close> or as regular function \<^verbatim>\<open>fn a => b\<close> of
    1.26 +  type \<^verbatim>\<open>'a -> 'b\<close>. Both forms occur routinely, and special care is required
    1.27 +  to tell them apart --- the static type-system of SML is only of limited help
    1.28    here.
    1.29  
    1.30 -  The first form is more intuitive: some combinator \<open>(unit -> 'a) -> 'a\<close>
    1.31 -  applies the given function to \<open>()\<close> to initiate the postponed evaluation
    1.32 -  process. The second form is more flexible: some combinator \<open>('a -> 'b) -> 'a
    1.33 -  -> 'b\<close> acts like a modified form of function application; several such
    1.34 -  combinators may be cascaded to modify a given function, before it is
    1.35 -  ultimately applied to some argument.
    1.36 +  The first form is more intuitive: some combinator \<^verbatim>\<open>(unit -> 'a) -> 'a\<close>
    1.37 +  applies the given function to \<^verbatim>\<open>()\<close> to initiate the postponed evaluation
    1.38 +  process. The second form is more flexible: some combinator
    1.39 +  \<^verbatim>\<open>('a -> 'b) -> 'a -> 'b\<close> acts like a modified form of function application;
    1.40 +  several such combinators may be cascaded to modify a given function, before
    1.41 +  it is ultimately applied to some argument.
    1.42  
    1.43    \<^medskip>
    1.44    \<^emph>\<open>Reified results\<close> make the disjoint sum of regular values versions
     2.1 --- a/src/Doc/Implementation/Proof.thy	Fri Sep 08 19:55:18 2017 +0200
     2.2 +++ b/src/Doc/Implementation/Proof.thy	Sat Sep 09 16:51:55 2017 +0200
     2.3 @@ -101,7 +101,8 @@
     2.4    @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
     2.5    @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
     2.6    @{index_ML Variable.import: "bool -> thm list -> Proof.context ->
     2.7 -  ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context"} \\
     2.8 +  ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list)
     2.9 +    * Proof.context"} \\
    2.10    @{index_ML Variable.focus: "binding list option -> term -> Proof.context ->
    2.11    ((string * (string * typ)) list * term) * Proof.context"} \\
    2.12    \end{mldecls}