isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:ef1da1abee46
+:1fb8d62c88a0
 text {*
 During development you might find it necessary to inspect some data
 in your code. This can be done in a ``quick-and-dirty'' fashion using
-the function @{ML [indexc] "writeln"}. For example
+the function @{ML [index] "writeln"}. For example
 @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
 will print out @{text [quotes] "any string"} inside the response buffer
 of Isabelle.  This function expects a string as argument. If you develop under PolyML,
 then there is a convenient, though again ``quick-and-dirty'', method for
 converting values into strings, namely the function @{ML PolyML.makestring}:
 @{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""}
-However, @{ML makestring} only works if the type of what is converted is monomorphic
+However, @{ML [index] makestring} only works if the type of what is converted is monomorphic
 and not a function.
 The function @{ML "writeln"} should only be used for testing purposes, because any
 output this function generates will be overwritten as soon as an error is
 raised. For printing anything more serious and elaborate, the
-function @{ML tracing} is more appropriate. This function writes all output into
+function @{ML [index] tracing} is more appropriate. This function writes all output into
 a separate tracing buffer. For example:
 @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
 It is also possible to redirect the ``channel'' where the string @{text "foo"} is
 text {*
 Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"}
 will cause that all tracing information is printed into the file @{text "foo.bar"}.
-You can print out error messages with the function @{ML error}; for example:
+You can print out error messages with the function @{ML [index] error}; for example:
 @{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")"
 "Exception- ERROR \"foo\" raised
 At command \"ML\"."}
-(FIXME Mention how to work with @{ML Toplevel.debug} and @{ML Toplevel.profiling}.)
+(FIXME Mention how to work with @{ML [index] debug in Toplevel} and
+@{ML [index] profiling in Toplevel}.)
 *}
 (*
 ML {* reset Toplevel.debug *}
 text {*
 Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm}
 or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing
 them (see Section \ref{sec:pretty}),
 but  for quick-and-dirty solutions they are far too unwieldy. A simple way to transform
-a term into a string is to use the function @{ML Syntax.string_of_term}.
+a term into a string is to use the function @{ML [index] string_of_term in Syntax}.
 @{ML_response_fake [display,gray]
 "Syntax.string_of_term @{context} @{term \"1::nat\"}"
 "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
 This produces a string with some additional information encoded in it. The string
-can be properly printed by using the function @{ML writeln}.
+can be properly printed by using the function @{ML [index] writeln}.
 @{ML_response_fake [display,gray]
 "writeln (Syntax.string_of_term @{context} @{term \"1::nat\"})"
 "\"1\""}
 ML{*fun string_of_cterm ctxt t =
 Syntax.string_of_term ctxt (term_of t)*}
 text {*
-In this example the function @{ML term_of} extracts the @{ML_type term} from
+In this example the function @{ML [index] term_of} extracts the @{ML_type term} from
 a @{ML_type cterm}.  If there are more than one @{ML_type cterm}s to be
-printed, you can use the function @{ML commas} to separate them.
+printed, you can use the function @{ML [index] commas} to separate them.
 *}
 ML{*fun string_of_cterms ctxt ts =
 commas (map (string_of_cterm ctxt) ts)*}
 text {*
 The easiest way to get the string of a theorem is to transform it
-into a @{ML_type cterm} using the function @{ML crep_thm}.
+into a @{ML_type cterm} using the function @{ML [index] crep_thm}.
 *}
 ML{*fun string_of_thm ctxt thm =
 string_of_cterm ctxt (#prop (crep_thm thm))*}
 "writeln (string_of_thm @{context} @{thm conjI})"
 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 In order to improve the readability of theorems we convert
 these schematic variables into free variables using the
-function @{ML Variable.import_thms}.
+function @{ML [index] import_thms in Variable}.
 *}
 ML{*fun no_vars ctxt thm =
 let
 val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
 For beginners perhaps the most puzzling parts in the existing code of Isabelle are
 the combinators. At first they seem to greatly obstruct the
 comprehension of the code, but after getting familiar with them, they
 actually ease the understanding and also the programming.
-The simplest combinator is @{ML I}, which is just the identity function defined as
+The simplest combinator is @{ML [index] I}, which is just the identity function defined as
 *}
 ML{*fun I x = x*}
-text {* Another simple combinator is @{ML K}, defined as *}
+text {* Another simple combinator is @{ML [index] K}, defined as *}
 ML{*fun K x = fn _ => x*}
 text {*
-@{ML K} ``wraps'' a function around the argument @{text "x"}. However, this
+@{ML [index] K} ``wraps'' a function around the argument @{text "x"}. However, this
 function ignores its argument. As a result, @{ML K} defines a constant function
 always returning @{text x}.
-The next combinator is reverse application, @{ML "|>"}, defined as:
+The next combinator is reverse application, @{ML [index] "|>"}, defined as:
 *}
 ML{*fun x |> f = f x*}
 text {* While just syntactic sugar for the usual function application,
 |> Syntax.string_of_term @{context}
 |> writeln"
 "P z za zb"}
 You can read off this behaviour from how @{ML apply_fresh_args} is
-coded: in Line 2, the function @{ML fastype_of} calculates the type of the
+coded: in Line 2, the function @{ML [index] fastype_of} calculates the type of the
-function; @{ML binder_types} in the next line produces the list of argument
+function; @{ML [index] binder_types} in the next line produces the list of argument
 types (in the case above the list @{text "[nat, int, unit]"}); Line 4
 pairs up each type with the string  @{text "z"}; the
-function @{ML variant_frees in Variable} generates for each @{text "z"} a
+function @{ML [index] variant_frees in Variable} generates for each @{text "z"} a
 unique name avoiding the given @{text f}; the list of name-type pairs is turned
 into a list of variable terms in Line 6, which in the last line is applied
-by the function @{ML list_comb} to the function. In this last step we have to
+by the function @{ML [index] list_comb} to the function. In this last step we have to
-use the function @{ML curry}, because @{ML list_comb} expects the function and the
+use the function @{ML [index] curry}, because @{ML [index] list_comb} expects the
-variables list as a pair. This kind of functions is often needed when
+function and the variables list as a pair. This kind of functions is often needed when
 constructing terms and the infrastructure helps tremendously to avoid
 any name clashes. Consider for example:
 @{ML_response_fake [display,gray]
 "apply_fresh_args @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"} @{context}
 |> Syntax.string_of_term @{context}
 |> writeln"
 "za z zb"}
-The combinator @{ML "#>"} is the reverse function composition. It can be
+The combinator @{ML [index] "#>"} is the reverse function composition. It can be
 used to define the following function
 *}
 ML{*val inc_by_six =
 (fn x => x + 1)
 which is the function composed of first the increment-by-one function and then
 increment-by-two, followed by increment-by-three. Again, the reverse function
 composition allows you to read the code top-down.
 The remaining combinators described in this section add convenience for the
-``waterfall method'' of writing functions. The combinator @{ML tap} allows
+``waterfall method'' of writing functions. The combinator @{ML [index] tap} allows
 you to get hold of an intermediate result (to do some side-calculations for
 instance). The function
 *}
 |> tap (fn x => tracing (PolyML.makestring x))
 |> (fn x => x + 2)*}
 text {*
 increments the argument first by @{text "1"} and then by @{text "2"}. In the
-middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
+middle (Line 3), however, it uses @{ML [index] tap} for printing the ``plus-one''
-intermediate result inside the tracing buffer. The function @{ML tap} can
+intermediate result inside the tracing buffer. The function @{ML [index] tap} can
 only be used for side-calculations, because any value that is computed
 cannot be merged back into the ``main waterfall''. To do this, you can use
 the next combinator.
-The combinator @{ML "`"} (a backtick) is similar to @{ML tap}, but applies a
+The combinator @{ML [index] "`"} (a backtick) is similar to @{ML tap}, but applies a
 function to the value and returns the result together with the value (as a
 pair). For example the function
 *}
 ML{*fun inc_as_pair x =
 takes @{text x} as argument, and then increments @{text x}, but also keeps
 @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
 for x}. After that, the function increments the right-hand component of the
 pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
-The combinators @{ML "|>>"} and @{ML "||>"} are defined for
+The combinators @{ML [index] "|>>"} and @{ML [index] "||>"} are defined for
 functions manipulating pairs. The first applies the function to
 the first component of the pair, defined as
 *}
 ML{*fun (x, y) |>> f = (f x, y)*}
 *}
 ML{*fun (x, y) ||> f = (x, f y)*}
 text {*
-With the combinator @{ML "|->"} you can re-combine the elements from a pair.
+With the combinator @{ML [index] "|->"} you can re-combine the elements from a pair.
 This combinator is defined as
 *}
 ML{*fun (x, y) |-> f = f x y*}
 ML{*fun double x =
 x |>  (fn x => (x, x))
 |-> (fn x => fn y => x + y)*}
 text {*
-The combinator @{ML ||>>} plays a central rôle whenever your task is to update a
+The combinator @{ML [index] ||>>} plays a central rôle whenever your task is to update a
 theory and the update also produces a side-result (for example a theorem). Functions
 for such tasks return a pair whose second component is the theory and the fist
-component is the side-result. Using @{ML ||>>}, you can do conveniently the update
+component is the side-result. Using @{ML [index] ||>>}, you can do conveniently the update
 and also accumulate the side-results. Considder the following simple function.
 *}
 ML %linenosgray{*fun acc_incs x =
 x |> (fn x => ("", x))
 ||>> (fn x => (x, x + 1))
 ||>> (fn x => (x, x + 1))*}
 text {*
 The purpose of Line 2 is to just pair up the argument with a dummy value (since
-@{ML "||>>"} operates on pairs). Each of the next three lines just increment
+@{ML [index] "||>>"} operates on pairs). Each of the next three lines just increment
 the value by one, but also nest the intrermediate results to the left. For example
 @{ML_response [display,gray]
 "acc_incs 1"
 "((((\"\", 1), 2), 3), 4)"}
 (FIXME: maybe give a ``real world'' example)
 *}
 text {*
-Recall that @{ML "|>"} is the reverse function application. Recall also that
+Recall that @{ML [index] "|>"} is the reverse function application. Recall also that
 the related
-reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},
+reverse function composition is @{ML [index] "#>"}. In fact all the combinators
-@{ML "|>>"} , @{ML "||>"} and @{ML "||>>"} described above have related combinators for
+@{ML [index] "|->"}, @{ML [index] "|>>"} , @{ML [index] "||>"} and @{ML [index]
-function composition, namely @{ML "#->"}, @{ML "#>>"}, @{ML "##>"} and @{ML "##>>"}.
+"||>>"} described above have related combinators for
-Using @{ML "#->"}, for example, the function @{text double} can also be written as:
+function composition, namely @{ML [index] "#->"}, @{ML [index] "#>>"},
+@{ML [index] "##>"} and @{ML [index] "##>>"}.
+Using @{ML [index] "#->"}, for example, the function @{text double} can also be written as:
 *}
 ML{*val double =
 (fn x => (x, x))
 #-> (fn x => fn y => x + y)*}
 @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
 where @{text "@{theory}"} is an antiquotation that is substituted with the
 current theory (remember that we assumed we are inside the theory
 @{text FirstSteps}). The name of this theory can be extracted using
-the function @{ML "Context.theory_name"}.
+the function @{ML [index] theory_name in Context}.
 Note, however, that antiquotations are statically linked, that is their value is
 determined at ``compile-time'', not ``run-time''. For example the function
 *}
 in
 map #1 simps
 end*}
 text {*
-The function @{ML dest_ss in MetaSimplifier} returns a record containing all
+The function @{ML [index] dest_ss in MetaSimplifier} returns a record containing all
 information stored in the simpset, but we are only interested in the names of the
 simp-rules. Now you can feed in the current simpset into this function.
 The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.
 @{ML_response_fake [display,gray]
 @{ML_response [display,gray]
 "@{binding \"name\"}"
 "name"}
-An example where a binding is needed is the function @{ML define in
+An example where a binding is needed is the function @{ML [index] define in
 LocalTheory}.  This function is below used to define the constant @{term
 "TrueConj"} as the conjunction
 @{term "True \<and> True"}.
 *}
 "@{term \"(a::nat) + b = c\"}"
 "Const (\"op =\", \<dots>) $
 (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 will show the term @{term "(a::nat) + b = c"}, but printed using the internal
-representation corresponding to the datatype @{ML_type "term"} defined as follows:
+representation corresponding to the datatype @{ML_type [index] "term"} defined as follows:
 *}
 ML_val %linenosgray{*datatype term =
 Const of string * typ
 | Free of string * typ
 Abs (\"x\", \<dots>,
 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $
 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 There are a number of handy functions that are frequently used for
-constructing terms. One is the function @{ML list_comb}, which takes a term
+constructing terms. One is the function @{ML [index] list_comb}, which takes a term
 and a list of terms as arguments, and produces as output the term
 list applied to the term. For example
 @{ML_response_fake [display,gray]
 "list_comb (@{term \"P::nat\"}, [@{term \"True\"}, @{term \"False\"}])"
 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
-Another handy function is @{ML lambda}, which abstracts a variable
+Another handy function is @{ML [index] lambda}, which abstracts a variable
 in a term. For example
 @{ML_response_fake [display,gray]
 "lambda @{term \"x::nat\"} @{term \"(P::nat\<Rightarrow>bool) x\"}"
 "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
 then the variable @{text "Free (\"x\", \"bool\")"} is \emph{not} abstracted.
 This is a fundamental principle
 of Church-style typing, where variables with the same name still differ, if they
 have different type.
-There is also the function @{ML subst_free} with which terms can
+There is also the function @{ML [index] subst_free} with which terms can
 be replaced by other terms. For example below, we will replace in
 @{term "(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0 x"}
 the subterm @{term "(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0"} by @{term y}, and @{term x} by @{term True}.
 @{ML_response_fake [display,gray]
 "subst_free [(@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})]
 @{term \"(\<lambda>x::nat. x)\"}"
 "Free (\"x\", \"nat\")"}
 There are many convenient functions that construct specific HOL-terms. For
-example @{ML "HOLogic.mk_eq"} constructs an equality out of two terms.
+example @{ML [index] mk_eq in HOLogic} constructs an equality out of two terms.
 The types needed in this equality are calculated from the type of the
 arguments. For example
 @{ML_response_fake [gray,display]
 "writeln (Syntax.string_of_term @{context}
 "@{type_name \"list\"}" "\"List.list\""}
 (FIXME: Explain the following better.)
 Occasionally you have to calculate what the ``base'' name of a given
-constant is. For this you can use the function @{ML Sign.extern_const} or
+constant is. For this you can use the function @{ML [index] extern_const in Sign} or
-@{ML Long_Name.base_name}. For example:
+@{ML base_name in Long_Name}. For example:
 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
 The difference between both functions is that @{ML extern_const in Sign} returns
 the smallest name that is still unique, whereas @{ML base_name in Long_Name} always
 *}
 ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}
-text {* This can be equally written with the combinator @{ML "-->"} as: *}
+text {* This can be equally written with the combinator @{ML [index] "-->"} as: *}
 ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
 text {*
 If you want to construct a function type with more than one argument
-type, then you can use @{ML "--->"}.
+type, then you can use @{ML [index] "--->"}.
 *}
 ML{*fun make_fun_types tys ty = tys ---> ty *}
 text {*
-A handy function for manipulating terms is @{ML map_types}: it takes a
+A handy function for manipulating terms is @{ML [index] map_types}: it takes a
 function and applies it to every type in a term. You can, for example,
 change every @{typ nat} in a term into an @{typ int} using the function:
 *}
 ML{*fun nat_to_int ty =
 "map_types nat_to_int @{term \"a = (1::nat)\"}"
 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
 $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
 If you want to obtain the list of free type-variables of a term, you
-can use the function @{ML Term.add_tfrees} (similarly @{ML Term.add_tvars}
+can use the function @{ML [index] add_tfrees in Term}
-for the schematic type-variables). One would expect that such functions
+(similarly @{ML [index] add_tvars in Term} for the schematic type-variables).
+One would expect that such functions
 take a term as input and return a list of types. But their type is actually
 @{text[display] "Term.term -> (string * Term.sort) list -> (string * Term.sort) list"}
 that is they take, besides a term, also a list of type-variables as input.
 @{ML_response [gray,display]
 "Term.add_tfrees @{term \"(a,b)\"} []"
 "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}
-The reason for this definition is that @{ML Term.add_tfrees} can
+The reason for this definition is that @{ML add_tfrees in Term} can
 be easily folded over a list of terms. Similarly for all functions
 named @{text "add_"}some\_name in @{ML_file "Pure/term.ML"}.
 *}
 text {*
 You can freely construct and manipulate @{ML_type "term"}s and @{ML_type
 typ}es, since they are just arbitrary unchecked trees. However, you
 eventually want to see if a term is well-formed, or type-checks, relative to
-a theory.  Type-checking is done via the function @{ML cterm_of}, which
+a theory.  Type-checking is done via the function @{ML [index] cterm_of}, which
-converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified}
+converts a @{ML_type [index] term} into a @{ML_type [index] cterm}, a \emph{certified}
 term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are
 abstract objects that are guaranteed to be type-correct, and they can only
 be constructed via ``official interfaces''.
 \end{exercise}
 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains
 enough typing information (constants, free variables and abstractions all have typing
 information) so that it is always clear what the type of a term is.
-Given a well-typed term, the function @{ML type_of} returns the
+Given a well-typed term, the function @{ML [index] type_of} returns the
 type of a term. Consider for example:
 @{ML_response [display,gray]
 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
 @{ML_response_fake [display,gray]
 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})"
 "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
 Since the complete traversal might sometimes be too costly and
-not necessary, there is the function @{ML fastype_of}, which
+not necessary, there is the function @{ML [index] fastype_of}, which
 also returns the type of a term.
 @{ML_response [display,gray]
 "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
 where no error is detected.
 Sometimes it is a bit inconvenient to construct a term with
 complete typing annotations, especially in cases where the typing
 information is redundant. A short-cut is to use the ``place-holder''
-type @{ML "dummyT"} and then let type-inference figure out the
+type @{ML [index] dummyT} and then let type-inference figure out the
 complete type. An example is as follows:
 @{ML_response_fake [display,gray]
 "let
 val c = Const (@{const_name \"plus\"}, dummyT)
 For the functions @{text "assume"}, @{text "forall_elim"} etc
 see \isccite{sec:thms}. The basic functions for theorems are defined in
 @{ML_file "Pure/thm.ML"}.
 \end{readmore}
-(FIXME: handy functions working on theorems, like @{ML ObjectLogic.rulify} and so on)
+(FIXME: handy functions working on theorems, like @{ML [index] rulify in ObjectLogic} and so on)
 (FIXME: how to add case-names to goal states - maybe in the
 next section)
 *}
 @{ML_type "theory -> theory"}: the input theory is the current theory and the
 output the theory where the theory attribute has been stored.
 This is a fundamental principle in Isabelle. A similar situation occurs
 for example with declaring constants. The function that declares a
-constant on the ML-level is @{ML Sign.add_consts_i}.
+constant on the ML-level is @{ML [index] add_consts_i in Sign}.
 If you write\footnote{Recall that ML-code  needs to be
 enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.}
 *}
 ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}
 *}
 ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
 text {*
-where the function @{ML "Thm.rule_attribute"} expects a function taking a
+where the function @{ML [index] rule_attribute in Thm} expects a function taking a
 context (which we ignore in the code above) and a theorem (@{text thm}), and
 returns another theorem (namely @{text thm} resolved with the theorem
-@{thm [source] sym}: @{thm sym[no_vars]}).\footnote{The function @{ML RS} is explained
+@{thm [source] sym}: @{thm sym[no_vars]}).\footnote{The function @{ML [index] RS}
-in Section~\ref{sec:simpletacs}.} The function
+is explained in Section~\ref{sec:simpletacs}.} The function
-@{ML "Thm.rule_attribute"} then returns
+@{ML rule_attribute in Thm} then returns  an attribute.
-an attribute.
 Before we can use the attribute, we need to set it up. This can be done
 using the Isabelle command \isacommand{attribute\_setup} as follows:
 *}
 \begin{isabelle}
 \isacommand{thm}~@{text "test[my_sym]"}\\
 @{text "> "}~@{thm test[my_sym]}
 \end{isabelle}
-An alternative for setting up an attribute is the function @{ML Attrib.setup}.
+An alternative for setting up an attribute is the function @{ML [index] setup in Attrib}.
 So instead of using \isacommand{attribute\_setup}, you can also set up the
 attribute as follows:
 *}
 ML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
 ML{*fun MY_THEN thms =
 Thm.rule_attribute (fn _ => fn thm => foldl ((op RS) o swap) thm thms)*}
 text {*
 where @{ML swap} swaps the components of a pair. The setup of this theorem
-attribute uses the parser @{ML Attrib.thms}, which parses a list of
+attribute uses the parser @{ML thms in Attrib}, which parses a list of
 theorems.
 *}
 attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *}
 "resolving the list of theorems with the proved theorem"
 \end{isabelle}
 you get an exception indicating that the theorem @{thm [source] sym}
 does not resolve with meta-equations.
-The purpose of @{ML Thm.rule_attribute} is to directly manipulate theorems.
+The purpose of @{ML [index] rule_attribute in Thm} is to directly manipulate theorems.
 Another usage of theorem attributes is to add and delete theorems from stored data.
 For example the theorem attribute @{text "[simp]"} adds or deletes a theorem from the
-current simpset. For these applications, you can use @{ML Thm.declaration_attribute}.
+current simpset. For these applications, you can use @{ML [index] declaration_attribute in Thm}.
 To illustrate this function, let us introduce a reference containing a list
 of theorems.
 *}
 ML{*val my_thms = ref ([] : thm list)*}
 (my_thms := Thm.del_thm thm (!my_thms); ctxt)*}
 text {*
 These functions take a theorem and a context and, for what we are explaining
 here it is sufficient that they just return the context unchanged. They change
-however the reference @{ML my_thms}, whereby the function @{ML Thm.add_thm}
+however the reference @{ML my_thms}, whereby the function
-adds a theorem if it is not already included in the list, and @{ML
+@{ML [index] add_thm in Thm} adds a theorem if it is not already included in
-Thm.del_thm} deletes one (both functions use the predicate @{ML
+the list, and @{ML [index] del_thm in Thm} deletes one (both functions use the
-Thm.eq_thm_prop}, which compares theorems according to their proved
+predicate @{ML [index] eq_thm_prop in Thm}, which compares theorems according to
-propositions modulo alpha-equivalence).
+their proved propositions modulo alpha-equivalence).
 You can turn functions @{ML my_thm_add} and @{ML my_thm_del} into
 attributes with the code
 *}
 attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *}
 "maintaining a list of my_thms - rough test only!"
 text {*
-The parser @{ML Attrib.add_del} is a pre-defined parser for
+The parser @{ML [index] add_del in Attrib} is a pre-defined parser for
 adding and deleting lemmas. Now if you prove the next lemma
 and attach to it the attribute @{text "[my_thms]"}
 *}
 lemma trueI_2[my_thms]: "True" by simp
 @{ML_response_fake [display,gray]
 "!my_thms"
 "[\"True\", \"Suc (Suc 0) = 2\"]"}
 The theorem @{thm [source] trueI_2} only appears once, since the
-function @{ML Thm.add_thm} tests for duplicates, before extending
+function @{ML [index] add_thm in Thm} tests for duplicates, before extending
 the list. Deletion from the list works as follows:
 *}
 declare test[my_thms del]
 @{ML_response_fake [display,gray]
 "!my_thms"
 "[\"True\"]"}
-We used in this example two functions declared as @{ML Thm.declaration_attribute},
+We used in this example two functions declared as @{ML [index] declaration_attribute in Thm},
 but there can be any number of them. We just have to change the parser for reading
 the arguments accordingly.
 However, as said at the beginning of this example, using references for storing theorems is
 \emph{not} the received way of doing such things. The received way is to
 With theorem attribute @{text my_thms2} you can also nicely see why it
 is important to
 store data in a ``data slot'' and \emph{not} in a reference. Backtrack
 to the point just before the lemma @{thm [source] three} was proved and
-check the the content of @{ML_struct "MyThmsData"}: it should be empty.
+check the the content of @{ML_struct MyThmsData}: it should be empty.
 The addition has been properly retracted. Now consider the proof:
 *}
 lemma four[my_thms]: "4 = Suc (Suc (Suc (Suc 0)))" by simp
 ML {* LocalTheory.set_group *}
 *)
 section {* Storing Theorems\label{sec:storing} (TBD) *}
-text {* @{ML PureThy.add_thms_dynamic} *}
+text {* @{ML [index] add_thms_dynamic in PureThy} *}
 local_setup {*
 LocalTheory.note Thm.theoremK
 ((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *}
 sophisticated, Isabelle includes an infrastructure for properly formatting text.
 This infrastructure is loosely based on a paper by Oppen~\cite{Oppen80}. Most of
 its functions do not operate on @{ML_type string}s, but on instances of the
 type:
-@{ML_type [display, gray] "Pretty.T"}
+@{ML_type [display, gray, index] "Pretty.T"}
-The function @{ML "Pretty.str"} transforms a (plain) string into such a pretty
+The function @{ML str in Pretty} transforms a (plain) string into such a pretty
 type. For example
 @{ML_response_fake [display,gray]
 "Pretty.str \"test\"" "String (\"test\", 4)"}
 where the result indicates that we transformed a string with length 4. Once
 you have a pretty type, you can, for example, control where linebreaks may
 occur in case the text wraps over a line, or with how much indentation a
 text should be printed.  However, if you want to actually output the
 formatted text, you have to transform the pretty type back into a @{ML_type
-string}. This can be done with the function @{ML Pretty.string_of}. In what
+string}. This can be done with the function @{ML [index] string_of in Pretty}. In what
 follows we will use the following wrapper function for printing a pretty
 type:
 *}
 ML{*fun pprint prt = writeln (Pretty.string_of prt)*}
 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
 oooooooooooooobaaaaaaaaaaaar"}
 However by using pretty types you have the ability to indicate a possible
 linebreak for example at each space. You can achieve this with the function
-@{ML Pretty.breaks}, which expects a list of pretty types and inserts a
+@{ML [index] breaks in Pretty}, which expects a list of pretty types and inserts a
 possible linebreak in between every two elements in this list. To print
 this list of pretty types as a single string, we concatenate them
-with the function @{ML Pretty.blk} as follows:
+with the function @{ML [index] blk in Pretty} as follows:
 @{ML_response_fake [display,gray]
 "let
 val ptrs = map Pretty.str (space_explode \" \" test_str)
 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
 Here the layout of @{ML test_str} is much more pleasing to the
-eye. The @{ML "0"} in @{ML Pretty.blk} stands for no indentation
+eye. The @{ML "0"} in @{ML [index] blk in Pretty} stands for no indentation
 of the printed string. You can increase the indentation and obtain
 @{ML_response_fake [display,gray]
 "let
 val ptrs = map Pretty.str (space_explode \" \" test_str)
 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
 where starting from the second line the indent is 3. If you want
 that every line starts with the same indent, you can use the
-function @{ML Pretty.indent} as follows:
+function @{ML [index] indent in Pretty} as follows:
 @{ML_response_fake [display,gray]
 "let
 val ptrs = map Pretty.str (space_explode \" \" test_str)
 in
 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
 If you want to print out a list of items separated by commas and
 have the linebreaks handled properly, you can use the function
-@{ML Pretty.commas}. For example
+@{ML [index] commas in Pretty}. For example
 @{ML_response_fake [display,gray]
 "let
 val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
 in
 100016, 100017, 100018, 100019, 100020"}
 where @{ML upto} generates a list of integers. You can print this
 list out as an ``set'', that means enclosed inside @{text [quotes] "{"} and
 @{text [quotes] "}"}, and separated by commas using the function
-@{ML Pretty.enum}. For example
+@{ML [index] enum in Pretty}. For example
 *}
 text {*
 @{ML_response_fake [display,gray]
 end*}
 text {*
 In Line 3 we define a function that inserts according to spaces
 possible linebreaks into an (English). In Lines 4 and 5 we pretty-print
-the term and its type using the functions @{ML Syntax.pretty_term} and
+the term and its type using the functions @{ML [index] pretty_term in Syntax} and
-@{ML Syntax.pretty_typ}. We also use the function @{ML Pretty.quote}
+@{ML [index] pretty_typ in Syntax}. We also use the function @{ML [index] quote in Pretty}
 in order to enclose the term and type inside quotation marks. In Line
 9 we add a period right after the type without the possibility of a
 linebreak, because we do not want that a linebreak occurs there.
 Now you can write

changeset 256	1fb8d62c88a0
parent 255	ef1da1abee46
child 257	ce0f60d0351e