
diff -r b1a458a03a8e -r 74ba778b09c9 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Sat Oct 31 11:37:41 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Sun Nov 01 10:49:25 2009 +0100
@@ -483,7 +483,7 @@
 (*<*)oops(*>*)
 
 text {*
-  The function @{ML_ind  resolve_tac} is similar to @{ML rtac}, except that it
+  The function @{ML_ind resolve_tac in Tactic} is similar to @{ML rtac}, except that it
   expects a list of theorems as argument. From this list it will apply the
   first applicable theorem (later theorems that are also applicable can be
   explored via the lazy sequences mechanism). Given the code
@@ -679,7 +679,7 @@
 
   Similar but less powerful functions than @{ML FOCUS in Subgoal}, respectively
   @{ML SUBPROOF}, are 
-  @{ML_ind  SUBGOAL} and @{ML_ind  CSUBGOAL}. They allow you to 
+  @{ML_ind SUBGOAL in Tactical} and @{ML_ind CSUBGOAL in Tactical}. They allow you to 
   inspect a given subgoal (the former
   presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
   cterm}). With them you can implement a tactic that applies a rule according
@@ -1242,7 +1242,7 @@
   \end{isabelle}
 
 
-  \footnote{\bf FIXME: say something about @{ML_ind  COND} and COND'}
+  \footnote{\bf FIXME: say something about @{ML_ind COND in Tactical} and COND'}
   \footnote{\bf FIXME: PARALLEL-CHOICE PARALLEL-GOALS}
   
   \begin{readmore}
@@ -1531,7 +1531,7 @@
 
 text {*
   This behaviour is not because of simplification rules, but how the subgoaler, solver 
-  and looper are set up in @{ML_ind HOL_basic_ss}.
+  and looper are set up in @{ML HOL_basic_ss}.
 
   The simpset @{ML_ind HOL_ss} is an extension of @{ML HOL_basic_ss} containing 
   already many useful simplification and congruence rules for the logical 
@@ -1870,7 +1870,7 @@
   Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
   The function also takes a list of patterns that can trigger the simproc.
   Now the simproc is set up and can be explicitly added using
-  @{ML_ind  addsimprocs} to a simpset whenever
+  @{ML_ind addsimprocs in MetaSimplifier} to a simpset whenever
   needed. 
 
   Simprocs are applied from inside to outside and from left to right. You can
@@ -2159,7 +2159,7 @@
 
   This very primitive way of rewriting can be made more powerful by
   combining several conversions into one. For this you can use conversion
-  combinators. The simplest conversion combinator is @{ML_ind  then_conv}, 
+  combinators. The simplest conversion combinator is @{ML_ind then_conv in Conv}, 
   which applies one conversion after another. For example
 
   @{ML_response_fake [display,gray]
@@ -2176,7 +2176,7 @@
   @{thm [source] true_conj1}. (When running this example recall the 
   problem with the pretty-printer normalising all terms.)
 
-  The conversion combinator @{ML_ind  else_conv} tries out the 
+  The conversion combinator @{ML_ind else_conv in Conv} tries out the 
   first one, and if it does not apply, tries the second. For example 
 
   @{ML_response_fake [display,gray]
@@ -2194,7 +2194,7 @@
   does not fail, however, because the combinator @{ML else_conv in Conv} will then 
   try out @{ML all_conv in Conv}, which always succeeds.
 
-  The conversion combinator @{ML_ind  try_conv in Conv} constructs a conversion 
+  The conversion combinator @{ML_ind try_conv in Conv} constructs a conversion 
   which is tried out on a term, but in case of failure just does nothing.
   For example
   
@@ -2210,8 +2210,8 @@
   Apart from the function @{ML beta_conversion in Thm}, which is able to fully
   beta-normalise a term, the conversions so far are restricted in that they
   only apply to the outer-most level of a @{ML_type cterm}. In what follows we
-  will lift this restriction. The combinators @{ML_ind  fun_conv in Conv} 
-  and @{ML_ind  arg_conv in Conv} will apply
+  will lift this restriction. The combinators @{ML_ind fun_conv in Conv} 
+  and @{ML_ind arg_conv in Conv} will apply
   a conversion to the first, respectively second, argument of an application.  
   For example
 
@@ -2335,18 +2335,19 @@
   "?P \<or> \<not> ?P"}
 
   Finally, conversions can also be turned into tactics and then applied to
-  goal states. This can be done with the help of the function @{ML_ind  CONVERSION},
+  goal states. This can be done with the help of the function 
+  @{ML_ind CONVERSION in Tactical},
   and also some predefined conversion combinators that traverse a goal
   state. The combinators for the goal state are: 
 
   \begin{itemize}
-  \item @{ML_ind  params_conv in Conv} for converting under parameters
+  \item @{ML_ind params_conv in Conv} for converting under parameters
   (i.e.~where goals are of the form @{text "\<And>x. P x \<Longrightarrow> Q x"})
 
-  \item @{ML_ind  prems_conv in Conv} for applying a conversion to all
+  \item @{ML_ind prems_conv in Conv} for applying a conversion to all
   premises of a goal, and
 
-  \item @{ML_ind  concl_conv in Conv} for applying a conversion to the
+  \item @{ML_ind concl_conv in Conv} for applying a conversion to the
   conclusion of a goal.
   \end{itemize}
 
@@ -2436,7 +2437,7 @@
   corresponding to the left-hand and right-hand side of the meta-equality. The
   assumption in @{ML unabs_def} is that the right-hand side is an
   abstraction. We compute the possibly empty list of abstracted variables in
-  Line 4 using the function @{ML_ind strip_abs_vars}. For this we have to
+  Line 4 using the function @{ML_ind strip_abs_vars in Term}. For this we have to
   transform the @{ML_type cterm} into a @{ML_type term}. In Line 5 we
   importing these variables into the context @{ML_text ctxt'}, in order to
   export them again in Line 15.  In Line 8 we certify the list of variables,




