# HG changeset patch # User wenzelm # Date 1376831418 -7200 # Node ID 1958a5e65ea59e157725eafa241693febb37c3d8 # Parent 417cb0f713e0c556e67809c7727fef0fe6bee95e tuned; diff -r 417cb0f713e0 -r 1958a5e65ea5 src/Doc/IsarImplementation/Logic.thy --- a/src/Doc/IsarImplementation/Logic.thy Sun Aug 18 13:58:33 2013 +0200 +++ b/src/Doc/IsarImplementation/Logic.thy Sun Aug 18 15:10:18 2013 +0200 @@ -881,8 +881,7 @@ The @{text "TYPE"} constructor is the canonical representative of the unspecified type @{text "\ itself"}; it essentially injects the language of types into that of terms. There is specific notation - @{text "TYPE(\)"} for @{text "TYPE\<^bsub>\ - itself\<^esub>"}. + @{text "TYPE(\)"} for @{text "TYPE\<^bsub>\ itself\<^esub>"}. Although being devoid of any particular meaning, the term @{text "TYPE(\)"} accounts for the type @{text "\"} within the term language. In particular, @{text "TYPE(\)"} may be used as formal diff -r 417cb0f713e0 -r 1958a5e65ea5 src/Doc/IsarImplementation/ML.thy --- a/src/Doc/IsarImplementation/ML.thy Sun Aug 18 13:58:33 2013 +0200 +++ b/src/Doc/IsarImplementation/ML.thy Sun Aug 18 15:10:18 2013 +0200 @@ -800,7 +800,7 @@ reasoning.} Currying gives some flexiblity due to \emph{partial application}. A - function @{text "f: \\<^sub>1 \ \\<^bsub>2\<^esub> \ \"} can be applied to @{text "x: \\<^sub>1"} + function @{text "f: \\<^sub>1 \ \\<^sub>2 \ \"} can be applied to @{text "x: \\<^sub>1"} and the remaining @{text "(f x): \\<^sub>2 \ \"} passed to another function etc. How well this works in practice depends on the order of arguments. In the worst case, arguments are arranged erratically, @@ -904,8 +904,8 @@ parametrized by arguments of type @{text "\"}. Given @{text "a: \"} the partial application @{text "(f a): \ \ \"} operates homogeneously on @{text "\"}. This can be iterated naturally over a - list of parameters @{text "[a\<^sub>1, \, a\<^sub>n]"} as @{text "f a\<^sub>1 #> \ #> f - a\<^bsub>n\<^esub>\<^bsub>\<^esub>"}. The latter expression is again a function @{text "\ \ \"}. + list of parameters @{text "[a\<^sub>1, \, a\<^sub>n]"} as @{text "f a\<^sub>1 #> \ #> f a\<^sub>n"}. + The latter expression is again a function @{text "\ \ \"}. It can be applied to an initial configuration @{text "b: \"} to start the iteration over the given list of arguments: each @{text "a"} in @{text "a\<^sub>1, \, a\<^sub>n"} is applied consecutively by updating a