594             Pretty.big_list "Params2 from the predicate:" (map (pretty_cterm ctxt) params2), 

   594             Pretty.big_list "Params2 from the predicate:" (map (pretty_cterm ctxt) params2), 

   595             Pretty.big_list "Prems1 from the rule:" (map (pretty_thm ctxt) prems1),

   595             Pretty.big_list "Prems1 from the rule:" (map (pretty_thm ctxt) prems1),

   596             Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)] 

   596             Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)] 

   597 in 

   597 in 

   598   pps |> Pretty.chunks

   598   pps |> Pretty.chunks

   600 end*}

   601 end*}

   601 text_raw{*

   603 text_raw{*

   602 \end{isabelle}

   604 \end{isabelle}

   603 \end{minipage}

   605 \end{minipage}

   604 \caption{A helper function that prints out the parameters and premises that

   606 \caption{A helper function that prints out the parameters and premises that

   605   need to be treated differently.\label{fig:chopprint}}

   607   need to be treated differently.\label{fig:chopprint}}

   786   Section~\ref{sec:nutshell}, we have  not yet dealt with the case where 

   788   Section~\ref{sec:nutshell}, we have  not yet dealt with the case where 

   787   recursive premises have preconditions. The introduction rule

   789   recursive premises have preconditions. The introduction rule

   788   of the accessible part is such a rule. 

   790   of the accessible part is such a rule. 

   789 *}

   791 *}

   790 

   792 

   791 lemma accpartI:

   794 lemma accpartI:

   792 shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

   795 shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

   793 apply(tactic {* expand_tac @{thms accpart_def} *})

   796 apply(tactic {* expand_tac @{thms accpart_def} *})

   794 apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} 1 *})

   797 apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} 1 *})

   795 apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} 1 *})

   798 apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} 1 *})