491 text \<open>

   491 text \<open>

   492   The function @{ML all_elims} takes a list of (certified) terms and instantiates

   492   The function @{ML all_elims} takes a list of (certified) terms and instantiates

   493   theorems of the form @{thm [source] all_elims_test}. For example we can instantiate

   493   theorems of the form @{thm [source] all_elims_test}. For example we can instantiate

   494   the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows:

   494   the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows:

   495 

   495 

   497 "let

   497 "let

   498   val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]

   498   val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]

   499   val new_thm = all_elims ctrms @{thm all_elims_test}

   499   val new_thm = all_elims ctrms @{thm all_elims_test}

   500 in

   500 in

   501   pwriteln (pretty_thm_no_vars @{context} new_thm)

   501   pwriteln (pretty_thm_no_vars @{context} new_thm)

   508 

   508 

   509   Similarly, the function @{ML imp_elims} eliminates preconditions from implications. 

   509   Similarly, the function @{ML imp_elims} eliminates preconditions from implications. 

   510   For example we can eliminate the preconditions \<open>A\<close> and \<open>B\<close> from

   510   For example we can eliminate the preconditions \<open>A\<close> and \<open>B\<close> from

   511   @{thm [source] imp_elims_test}:

   511   @{thm [source] imp_elims_test}:

   512 

   512 

   514 "let

   514 "let

   515   val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}

   515   val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}

   516 in

   516 in

   517   pwriteln (pretty_thm_no_vars @{context} res)

   517   pwriteln (pretty_thm_no_vars @{context} res)

   518 end"

   518 end"