# HG changeset patch # User wenzelm # Date 1504968715 -7200 # Node ID 49318345c33231d677ebe3456ed0f6300ceff536 # Parent bcea02893d17d453f6a61f216e5319a3e5773cb3 tuned; diff -r bcea02893d17 -r 49318345c332 src/Doc/Implementation/ML.thy --- a/src/Doc/Implementation/ML.thy Fri Sep 08 19:55:18 2017 +0200 +++ b/src/Doc/Implementation/ML.thy Sat Sep 09 16:51:55 2017 +0200 @@ -946,9 +946,9 @@ Another benefit of @{ML add_content} is its ``open'' form as a function on buffers that can be continued in further linear transformations, folding etc. Thus it is more compositional than the naive @{ML slow_content}. As - realistic example, compare the old-style @{ML "Term.maxidx_of_term: term -> - int"} with the newer @{ML "Term.maxidx_term: term -> int -> int"} in - Isabelle/Pure. + realistic example, compare the old-style + @{ML "Term.maxidx_of_term: term -> int"} with the newer @{ML + "Term.maxidx_term: term -> int -> int"} in Isabelle/Pure. Note that @{ML fast_content} above is only defined as example. In many practical situations, it is customary to provide the incremental @{ML @@ -1851,18 +1851,18 @@ evaluation via promises, evaluation with time limit etc. \<^medskip> - An \<^emph>\unevaluated expression\ is represented either as unit abstraction \<^verbatim>\fn - () => a\ of type \<^verbatim>\unit -> 'a\ or as regular function \<^verbatim>\fn a => b\ of type - \<^verbatim>\'a -> 'b\. Both forms occur routinely, and special care is required to - tell them apart --- the static type-system of SML is only of limited help + An \<^emph>\unevaluated expression\ is represented either as unit abstraction + \<^verbatim>\fn () => a\ of type \<^verbatim>\unit -> 'a\ or as regular function \<^verbatim>\fn a => b\ of + type \<^verbatim>\'a -> 'b\. Both forms occur routinely, and special care is required + to tell them apart --- the static type-system of SML is only of limited help here. - The first form is more intuitive: some combinator \(unit -> 'a) -> 'a\ - applies the given function to \()\ to initiate the postponed evaluation - process. The second form is more flexible: some combinator \('a -> 'b) -> 'a - -> 'b\ acts like a modified form of function application; several such - combinators may be cascaded to modify a given function, before it is - ultimately applied to some argument. + The first form is more intuitive: some combinator \<^verbatim>\(unit -> 'a) -> 'a\ + applies the given function to \<^verbatim>\()\ to initiate the postponed evaluation + process. The second form is more flexible: some combinator + \<^verbatim>\('a -> 'b) -> 'a -> 'b\ acts like a modified form of function application; + several such combinators may be cascaded to modify a given function, before + it is ultimately applied to some argument. \<^medskip> \<^emph>\Reified results\ make the disjoint sum of regular values versions diff -r bcea02893d17 -r 49318345c332 src/Doc/Implementation/Proof.thy --- a/src/Doc/Implementation/Proof.thy Fri Sep 08 19:55:18 2017 +0200 +++ b/src/Doc/Implementation/Proof.thy Sat Sep 09 16:51:55 2017 +0200 @@ -101,7 +101,8 @@ @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\ @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\ @{index_ML Variable.import: "bool -> thm list -> Proof.context -> - ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context"} \\ + ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) + * Proof.context"} \\ @{index_ML Variable.focus: "binding list option -> term -> Proof.context -> ((string * (string * typ)) list * term) * Proof.context"} \\ \end{mldecls}