equal
deleted
inserted
replaced
184 TRY o simp_tac (add_ss thms2), |
184 TRY o simp_tac (add_ss thms2), |
185 TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts)))] i |
185 TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts)))] i |
186 end) |
186 end) |
187 in |
187 in |
188 induct_prove qtys (goals1 @ goals2) qinduct tac ctxt |
188 induct_prove qtys (goals1 @ goals2) qinduct tac ctxt |
|
189 |> map atomize |
|
190 |> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]})) |
189 end |
191 end |
190 |
192 |
191 |
193 |
192 |
194 |
193 end (* structure *) |
195 end (* structure *) |