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 \ \ ?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 "\x. P x \ 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,