131 

   131 

   132 ML {*

   132 ML {*

   133 fun lift_thm_my_int lthy t =

   133 fun lift_thm_my_int lthy t =

   134   lift_thm lthy qty ty_name rsp_thms defs t

   134   lift_thm lthy qty ty_name rsp_thms defs t

   135 *}

   135 *}

   136 

   138 

   137 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *}

   139 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *}

   138 

   140 

   139 lemma plus_assoc_pre:

   141 lemma plus_assoc_pre:

   140   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"

   142   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"