536 text_raw{*

   536 text_raw{*

   537 \begin{figure}[t]

   537 \begin{figure}[t]

   538 \begin{minipage}{\textwidth}

   538 \begin{minipage}{\textwidth}

   539 \begin{isabelle}

   539 \begin{isabelle}

   540 *}

   540 *}

   541 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 

   543 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 

   542 let 

   544 let 

   544   val string_of_asms = string_of_cterms context asms

   547   val string_of_asms = string_of_cterms context asms

   545   val string_of_concl = string_of_cterm context concl

   548   val string_of_concl = string_of_cterm context concl

   546   val string_of_prems = string_of_thms_no_vars context prems   

   549   val string_of_prems = string_of_thms_no_vars context prems   

   547   val string_of_schms = string_of_cterms context (snd schematics)    

   550   val string_of_schms = string_of_cterms context (snd schematics)    

   548  

   551  

   549   val _ = (writeln ("params: " ^ string_of_params);

   552   val _ = (writeln ("params: " ^ string_of_params);

   550            writeln ("schematics: " ^ string_of_schms);

   554            writeln ("schematics: " ^ string_of_schms);

   551            writeln ("assumptions: " ^ string_of_asms);

   555            writeln ("assumptions: " ^ string_of_asms);

   552            writeln ("conclusion: " ^ string_of_concl);

   556            writeln ("conclusion: " ^ string_of_concl);

   553            writeln ("premises: " ^ string_of_prems))

   557            writeln ("premises: " ^ string_of_prems))

   554 in

   558 in

   561  @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for

   565  @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for

   562   extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}

   566   extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}

   563 \end{figure}

   567 \end{figure}

   564 *}

   568 *}

   565 

   569 

   567 lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"

   570 lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"

   568 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?

   571 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?

   569 

   572 

   570 txt {*

   573 txt {*

   571   The tactic produces the following printout:

   574   The tactic produces the following printout:

  1054 

  1057 

  1055 text {*

  1058 text {*

  1056   will solve all trivial subgoals involving @{term True} or @{term "False"}.

  1059   will solve all trivial subgoals involving @{term True} or @{term "False"}.

  1057 

  1060 

  1058   (FIXME: say something about @{ML [index] COND} and COND')

  1061   (FIXME: say something about @{ML [index] COND} and COND')

  1059   

  1064   

  1060   \begin{readmore}

  1065   \begin{readmore}

  1061   Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.

  1066   Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.

  1062   Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.

  1067   Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.

  1063   \end{readmore}

  1068   \end{readmore}