equal
deleted
inserted
replaced
248 |> map (fn thm => thm RS @{thm sym}) |
248 |> map (fn thm => thm RS @{thm sym}) |
249 |
249 |
250 val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) |
250 val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) |
251 |
251 |
252 val (alpha_eqvt, lthy6) = |
252 val (alpha_eqvt, lthy6) = |
253 Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 |
253 Nominal_Eqvt.raw_equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 |
254 |
254 |
255 val _ = trace_msg (K "Proving equivalence of alpha...") |
255 val _ = trace_msg (K "Proving equivalence of alpha...") |
256 val alpha_refl_thms = |
256 val alpha_refl_thms = |
257 raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy6 |
257 raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy6 |
258 |
258 |