1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy Mon Oct 22 21:32:12 2007 +0200
1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy Tue Oct 23 10:53:15 2007 +0200
1.3 @@ -296,8 +296,6 @@
1.4 text %mlref {*
1.5 \begin{mldecls}
1.6 @{index_ML "op |> ": "'a * ('a -> 'b) -> 'b"} \\
1.7 - @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
1.8 - @{index_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
1.9 \end{mldecls}
1.10 *}
1.11
1.12 @@ -305,8 +303,6 @@
1.13 typedecl foo
1.14 consts foo :: foo
1.15 ML {*
1.16 -val dummy_const = ("bar", @{typ foo}, NoSyn)
1.17 -val dummy_def = ("bar", @{term foo})
1.18 val thy = Theory.copy @{theory}
1.19 *}
1.20 (*>*)
1.21 @@ -317,22 +313,30 @@
1.22 particular value @{text "x \<Colon> foo"} which is then transformed
1.23 by application of a function @{text "f \<Colon> foo \<Rightarrow> foo"},
1.24 continued by an application of a function @{text "g \<Colon> foo \<Rightarrow> bar"},
1.25 - and so on. As a canoncial example, take primitive functions enriching
1.26 - theories by constants and definitions:
1.27 - @{ML "Sign.add_consts_i: (string * typ * mixfix) list -> theory
1.28 --> theory"}
1.29 - and @{ML "Theory.add_defs_i: bool -> bool
1.30 --> (bstring * term) list -> theory -> theory"}.
1.31 - Written with naive application, an addition of a constant with
1.32 - a corresponding definition would look like:
1.33 - @{ML "Theory.add_defs_i false false [dummy_def]
1.34 - (Sign.add_consts_i [dummy_const] thy)"}.
1.35 - With increasing numbers of applications, this code gets quite unreadable.
1.36 - Using composition, at least the nesting of brackets may be reduced:
1.37 - @{ML "(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i
1.38 - [dummy_const]) thy"}.
1.39 - What remains unsatisfactory is that things are written down in the opposite order
1.40 - as they actually ``happen''.
1.41 + and so on. As a canoncial example, take functions enriching
1.42 + a theory by constant declararion and primitive definitions:
1.43 +
1.44 + \begin{quotation}
1.45 + @{ML "Sign.declare_const: Markup.property list -> bstring * typ * mixfix
1.46 + -> theory -> term * theory"}
1.47 +
1.48 + @{ML "Thm.add_def: bool -> bstring * term -> theory -> thm * theory"}
1.49 + \end{quotation}
1.50 +
1.51 + Written with naive application, an addition of constant
1.52 + @{text bar} with type @{typ "foo \<Rightarrow> foo"} and
1.53 + a corresponding definition @{term "bar \<equiv> \<lambda>x. x"} would look like:
1.54 +
1.55 + \begin{quotation}
1.56 + @{ML "(fn (t, thy) => Thm.add_def false
1.57 + (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
1.58 + (Sign.declare_const []
1.59 + (\"bar\", @{typ \"foo => foo\"}, NoSyn) thy)"}.
1.60 + \end{quotation}
1.61 +
1.62 + With increasing numbers of applications, this code gets quite
1.63 + unreadable. Further, it is unintuitive that things are
1.64 + written down in the opposite order as they actually ``happen''.
1.65 *}
1.66
1.67 (*<*)
1.68 @@ -342,18 +346,15 @@
1.69 (*>*)
1.70
1.71 text {*
1.72 - At this stage, Isabelle offers some combinators which allow for more convenient
1.73 - notation, most notably reverse application:
1.74 - @{ML "
1.75 -thy
1.76 -|> Sign.add_consts_i [dummy_const]
1.77 -|> Theory.add_defs_i false false [dummy_def]"}
1.78 -*}
1.79 -
1.80 -text {*
1.81 - \noindent When iterating over a list of parameters @{text "[x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<Colon> 'a list"},
1.82 - the @{ML fold} combinator lifts a single function @{text "f \<Colon> 'a -> 'b -> 'b"}:
1.83 - @{text "y |> fold f [x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<equiv> y |> f x\<^isub>1 |> f x\<^isub>2 |> \<dots> |> f x\<^isub>n"}
1.84 + \noindent At this stage, Isabelle offers some combinators which allow
1.85 + for more convenient notation, most notably reverse application:
1.86 + \begin{quotation}
1.87 +@{ML "thy
1.88 +|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
1.89 +|> (fn (t, thy) => thy
1.90 +|> Thm.add_def false
1.91 + (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
1.92 + \end{quotation}
1.93 *}
1.94
1.95 text %mlref {*
1.96 @@ -362,12 +363,78 @@
1.97 @{index_ML "op |>> ": "('a * 'c) * ('a -> 'b) -> 'b * 'c"} \\
1.98 @{index_ML "op ||> ": "('c * 'a) * ('a -> 'b) -> 'c * 'b"} \\
1.99 @{index_ML "op ||>> ": "('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b"} \\
1.100 + \end{mldecls}
1.101 +*}
1.102 +
1.103 +text {*
1.104 + \noindent Usually, functions involving theory updates also return
1.105 + side results; to use these conveniently, yet another
1.106 + set of combinators is at hand, most notably @{ML "op |->"}
1.107 + which allows curried access to side results:
1.108 + \begin{quotation}
1.109 +@{ML "thy
1.110 +|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
1.111 +|-> (fn t => Thm.add_def false
1.112 + (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
1.113 +"}
1.114 + \end{quotation}
1.115 +
1.116 + \noindent @{ML "op |>>"} allows for processing side results on their own:
1.117 + \begin{quotation}
1.118 +@{ML "thy
1.119 +|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
1.120 +|>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
1.121 +|-> (fn def => Thm.add_def false (\"bar_def\", def))
1.122 +"}
1.123 + \end{quotation}
1.124 +
1.125 + \noindent Orthogonally, @{ML "op ||>"} applies a transformation
1.126 + in the presence of side results which are left unchanged:
1.127 + \begin{quotation}
1.128 +@{ML "thy
1.129 +|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
1.130 +||> Sign.add_path \"foobar\"
1.131 +|-> (fn t => Thm.add_def false
1.132 + (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
1.133 +||> Sign.restore_naming thy
1.134 +"}
1.135 + \end{quotation}
1.136 +
1.137 + \noindent @{index_ML "op ||>>"} accumulates side results:
1.138 + \begin{quotation}
1.139 +@{ML "thy
1.140 +|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
1.141 +||>> Sign.declare_const [] (\"foobar\", @{typ \"foo => foo\"}, NoSyn)
1.142 +|-> (fn (t1, t2) => Thm.add_def false
1.143 + (\"bar_def\", Logic.mk_equals (t1, t2)))
1.144 +"}
1.145 + \end{quotation}
1.146 +*}
1.147 +
1.148 +text %mlref {*
1.149 + \begin{mldecls}
1.150 + @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
1.151 @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\
1.152 \end{mldecls}
1.153 *}
1.154
1.155 text {*
1.156 - \noindent FIXME transformations involving side results
1.157 + \noindent This principles naturally lift to @{text lists} using
1.158 + the @{ML fold} and @{ML fold_map} combinators.
1.159 + The first lifts a single function
1.160 + @{text "f \<Colon> 'a -> 'b -> 'b"} to @{text "'a list -> 'b -> 'b"}
1.161 + such that
1.162 + @{text "y |> fold f [x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<equiv> y |> f x\<^isub>1 |> f x\<^isub>2 |> \<dots> |> f x\<^isub>n"};
1.163 + the second accumulates side results in a list by lifting
1.164 + a single function
1.165 + @{text "f \<Colon> 'a -> 'b -> 'c \<times> 'b"} to @{text "'a list -> 'b -> 'c list \<times> 'b"}
1.166 + such that
1.167 + @{text "y |> fold_map f [x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<equiv> y |> f x\<^isub>1 ||>> f x\<^isub>2 ||>> \<dots> ||>> f x\<^isub>n
1.168 + ||> (fn ((z\<^isub>1, z\<^isub>2), \<dots> z\<^isub>n) => [z\<^isub>1, z\<^isub>2, \<dots> z\<^isub>n])"};
1.169 +
1.170 + Example: FIXME
1.171 + \begin{quotation}
1.172 + \end{quotation}
1.173 *}
1.174
1.175 text %mlref {*
1.176 @@ -438,7 +505,7 @@
1.177
1.178 text {*
1.179 Lists are often used as set-like data structures -- set-like in
1.180 - then sense that they support notion of @{ML member}-ship,
1.181 + the sense that they support a notion of @{ML member}-ship,
1.182 @{ML insert}-ing and @{ML remove}-ing, but are order-sensitive.
1.183 This is convenient when implementing a history-like mechanism:
1.184 @{ML insert} adds an element \emph{to the front} of a list,
2.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex Mon Oct 22 21:32:12 2007 +0200
2.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue Oct 23 10:53:15 2007 +0200
2.3 @@ -339,8 +339,6 @@
2.4 \begin{isamarkuptext}%
2.5 \begin{mldecls}
2.6 \indexml{op |$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
2.7 - \indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
2.8 - \indexml{fold-rev}\verb|fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
2.9 \end{mldecls}%
2.10 \end{isamarkuptext}%
2.11 \isamarkuptrue%
2.12 @@ -371,22 +369,30 @@
2.13 particular value \isa{x\ {\isasymColon}\ foo} which is then transformed
2.14 by application of a function \isa{f\ {\isasymColon}\ foo\ {\isasymRightarrow}\ foo},
2.15 continued by an application of a function \isa{g\ {\isasymColon}\ foo\ {\isasymRightarrow}\ bar},
2.16 - and so on. As a canoncial example, take primitive functions enriching
2.17 - theories by constants and definitions:
2.18 - \verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory|\isasep\isanewline%
2.19 -\verb|-> theory|
2.20 - and \verb|Theory.add_defs_i: bool -> bool|\isasep\isanewline%
2.21 -\verb|-> (bstring * term) list -> theory -> theory|.
2.22 - Written with naive application, an addition of a constant with
2.23 - a corresponding definition would look like:
2.24 - \verb|Theory.add_defs_i false false [dummy_def]|\isasep\isanewline%
2.25 -\verb| (Sign.add_consts_i [dummy_const] thy)|.
2.26 - With increasing numbers of applications, this code gets quite unreadable.
2.27 - Using composition, at least the nesting of brackets may be reduced:
2.28 - \verb|(Theory.add_defs_i false false [dummy_def] o Sign.add_consts_i|\isasep\isanewline%
2.29 -\verb| [dummy_const]) thy|.
2.30 - What remains unsatisfactory is that things are written down in the opposite order
2.31 - as they actually ``happen''.%
2.32 + and so on. As a canoncial example, take functions enriching
2.33 + a theory by constant declararion and primitive definitions:
2.34 +
2.35 + \begin{quotation}
2.36 + \verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix|\isasep\isanewline%
2.37 +\verb| -> theory -> term * theory|
2.38 +
2.39 + \verb|Thm.add_def: bool -> bstring * term -> theory -> thm * theory|
2.40 + \end{quotation}
2.41 +
2.42 + Written with naive application, an addition of constant
2.43 + \isa{bar} with type \isa{foo\ {\isasymRightarrow}\ foo} and
2.44 + a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like:
2.45 +
2.46 + \begin{quotation}
2.47 + \verb|(fn (t, thy) => Thm.add_def false|\isasep\isanewline%
2.48 +\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
2.49 +\verb| (Sign.declare_const []|\isasep\isanewline%
2.50 +\verb| ("bar", @{typ "foo => foo"}, NoSyn) thy)|.
2.51 + \end{quotation}
2.52 +
2.53 + With increasing numbers of applications, this code gets quite
2.54 + unreadable. Further, it is unintuitive that things are
2.55 + written down in the opposite order as they actually ``happen''.%
2.56 \end{isamarkuptext}%
2.57 \isamarkuptrue%
2.58 %
2.59 @@ -404,19 +410,15 @@
2.60 \endisadelimML
2.61 %
2.62 \begin{isamarkuptext}%
2.63 -At this stage, Isabelle offers some combinators which allow for more convenient
2.64 - notation, most notably reverse application:
2.65 - \isasep\isanewline%
2.66 +\noindent At this stage, Isabelle offers some combinators which allow
2.67 + for more convenient notation, most notably reverse application:
2.68 + \begin{quotation}
2.69 \verb|thy|\isasep\isanewline%
2.70 -\verb||\verb,|,\verb|> Sign.add_consts_i [dummy_const]|\isasep\isanewline%
2.71 -\verb||\verb,|,\verb|> Theory.add_defs_i false false [dummy_def]|%
2.72 -\end{isamarkuptext}%
2.73 -\isamarkuptrue%
2.74 -%
2.75 -\begin{isamarkuptext}%
2.76 -\noindent When iterating over a list of parameters \isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymColon}\ {\isacharprime}a\ list},
2.77 - the \verb|fold| combinator lifts a single function \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b}:
2.78 - \isa{y\ {\isacharbar}{\isachargreater}\ fold\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}\ y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub n}%
2.79 +\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
2.80 +\verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline%
2.81 +\verb||\verb,|,\verb|> Thm.add_def false|\isasep\isanewline%
2.82 +\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
2.83 + \end{quotation}%
2.84 \end{isamarkuptext}%
2.85 \isamarkuptrue%
2.86 %
2.87 @@ -432,6 +434,72 @@
2.88 \indexml{op |$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\
2.89 \indexml{op ||$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\
2.90 \indexml{op ||$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\
2.91 + \end{mldecls}%
2.92 +\end{isamarkuptext}%
2.93 +\isamarkuptrue%
2.94 +%
2.95 +\endisatagmlref
2.96 +{\isafoldmlref}%
2.97 +%
2.98 +\isadelimmlref
2.99 +%
2.100 +\endisadelimmlref
2.101 +%
2.102 +\begin{isamarkuptext}%
2.103 +\noindent Usually, functions involving theory updates also return
2.104 + side results; to use these conveniently, yet another
2.105 + set of combinators is at hand, most notably \verb|op |\verb,|,\verb|->|
2.106 + which allows curried access to side results:
2.107 + \begin{quotation}
2.108 +\verb|thy|\isasep\isanewline%
2.109 +\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
2.110 +\verb||\verb,|,\verb|-> (fn t => Thm.add_def false|\isasep\isanewline%
2.111 +\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
2.112 +
2.113 + \end{quotation}
2.114 +
2.115 + \noindent \verb|op |\verb,|,\verb|>>| allows for processing side results on their own:
2.116 + \begin{quotation}
2.117 +\verb|thy|\isasep\isanewline%
2.118 +\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
2.119 +\verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
2.120 +\verb||\verb,|,\verb|-> (fn def => Thm.add_def false ("bar_def", def))|\isasep\isanewline%
2.121 +
2.122 + \end{quotation}
2.123 +
2.124 + \noindent Orthogonally, \verb|op |\verb,|,\verb||\verb,|,\verb|>| applies a transformation
2.125 + in the presence of side results which are left unchanged:
2.126 + \begin{quotation}
2.127 +\verb|thy|\isasep\isanewline%
2.128 +\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
2.129 +\verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline%
2.130 +\verb||\verb,|,\verb|-> (fn t => Thm.add_def false|\isasep\isanewline%
2.131 +\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
2.132 +\verb||\verb,|,\verb||\verb,|,\verb|> Sign.restore_naming thy|\isasep\isanewline%
2.133 +
2.134 + \end{quotation}
2.135 +
2.136 + \noindent \indexml{op ||$>$$>$}\verb|op |\verb,|,\verb||\verb,|,\verb|>>| accumulates side results:
2.137 + \begin{quotation}
2.138 +\verb|thy|\isasep\isanewline%
2.139 +\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
2.140 +\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ("foobar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
2.141 +\verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false|\isasep\isanewline%
2.142 +\verb| ("bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
2.143 +
2.144 + \end{quotation}%
2.145 +\end{isamarkuptext}%
2.146 +\isamarkuptrue%
2.147 +%
2.148 +\isadelimmlref
2.149 +%
2.150 +\endisadelimmlref
2.151 +%
2.152 +\isatagmlref
2.153 +%
2.154 +\begin{isamarkuptext}%
2.155 +\begin{mldecls}
2.156 + \indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
2.157 \indexml{fold-map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
2.158 \end{mldecls}%
2.159 \end{isamarkuptext}%
2.160 @@ -445,7 +513,21 @@
2.161 \endisadelimmlref
2.162 %
2.163 \begin{isamarkuptext}%
2.164 -\noindent FIXME transformations involving side results%
2.165 +\noindent This principles naturally lift to \isa{lists} using
2.166 + the \verb|fold| and \verb|fold_map| combinators.
2.167 + The first lifts a single function
2.168 + \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b} to \isa{{\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b}
2.169 + such that
2.170 + \isa{y\ {\isacharbar}{\isachargreater}\ fold\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}\ y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub n};
2.171 + the second accumulates side results in a list by lifting
2.172 + a single function
2.173 + \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}c\ {\isasymtimes}\ {\isacharprime}b} to \isa{{\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}c\ list\ {\isasymtimes}\ {\isacharprime}b}
2.174 + such that
2.175 + \isa{y\ {\isacharbar}{\isachargreater}\ fold{\isacharunderscore}map\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}\ y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ f\ x\isactrlisub n\ {\isacharbar}{\isacharbar}{\isachargreater}\ {\isacharparenleft}fn\ {\isacharparenleft}{\isacharparenleft}z\isactrlisub {\isadigit{1}}{\isacharcomma}\ z\isactrlisub {\isadigit{2}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}\ z\isactrlisub n{\isacharparenright}\ {\isacharequal}{\isachargreater}\ {\isacharbrackleft}z\isactrlisub {\isadigit{1}}{\isacharcomma}\ z\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ z\isactrlisub n{\isacharbrackright}{\isacharparenright}};
2.176 +
2.177 + Example: FIXME
2.178 + \begin{quotation}
2.179 + \end{quotation}%
2.180 \end{isamarkuptext}%
2.181 \isamarkuptrue%
2.182 %
2.183 @@ -568,7 +650,7 @@
2.184 %
2.185 \begin{isamarkuptext}%
2.186 Lists are often used as set-like data structures -- set-like in
2.187 - then sense that they support notion of \verb|member|-ship,
2.188 + the sense that they support a notion of \verb|member|-ship,
2.189 \verb|insert|-ing and \verb|remove|-ing, but are order-sensitive.
2.190 This is convenient when implementing a history-like mechanism:
2.191 \verb|insert| adds an element \emph{to the front} of a list,
3.1 --- a/doc-src/IsarImplementation/Thy/document/isabelle.sty Mon Oct 22 21:32:12 2007 +0200
3.2 +++ b/doc-src/IsarImplementation/Thy/document/isabelle.sty Tue Oct 23 10:53:15 2007 +0200
3.3 @@ -25,10 +25,10 @@
3.4 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
3.5 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
3.6 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
3.7 -\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
3.8 -\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
3.9 -\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
3.10 -\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
3.11 +\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
3.12 +\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
3.13 +\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
3.14 +\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
3.15 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
3.16 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
3.17 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}