author | wenzelm |

Sat Sep 09 16:51:55 2017 +0200 (21 months ago) | |

changeset 66663 | 49318345c332 |

parent 66650 | bcea02893d17 |

child 66664 | 91fc9816a86f |

tuned;

src/Doc/Implementation/ML.thy | file | annotate | diff | revisions | |

src/Doc/Implementation/Proof.thy | file | annotate | diff | revisions |

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}