66 ML {*

    66 ML {*

    67   val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps

    67   val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps

    68     prod.cases}

    68     prod.cases}

    69 *}

    69 *}

    70 

    70 

    73 ML {*

    71 ML {*

    74  val thms_e = map (lift_thm @{context} qtys simps)  @{thms eq_iff}

    72  val thms_e = map (lift_thm @{context} qtys simps)  @{thms eq_iff}

    75 *}

    73 *}

    76 

    74 

    77 ML {*

    75 ML {*

    91   val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt}

    89   val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt}

    92 *}

    90 *}

    93 

    91 

    94 ML {*

    92 ML {*

    95   val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt}

    93   val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt}

   102 *}

    94 *}

   103 

    95 

   104 

    96 

   105 

    97 

   106 thm eq_iff

    98 thm eq_iff