397 val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
397 val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
398 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4) |
398 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4) |
399 |
399 |
400 val fv_eqvt = |
400 val fv_eqvt = |
401 if get_STEPS lthy > 7 |
401 if get_STEPS lthy > 7 |
402 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) lthy_tmp |
402 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) |
|
403 (Local_Theory.restore lthy_tmp) |
403 else raise TEST lthy4 |
404 else raise TEST lthy4 |
404 |
405 |
405 val lthy_tmp' = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) |
406 val lthy_tmp' = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) |
406 |
407 |
407 val (alpha_eqvt, _) = |
408 val (alpha_eqvt, _) = |
408 if get_STEPS lthy > 8 |
409 if get_STEPS lthy > 8 |
409 then Nominal_Eqvt.equivariance false alpha_trms alpha_induct alpha_intros lthy_tmp' |
410 then Nominal_Eqvt.equivariance false alpha_trms alpha_induct alpha_intros lthy_tmp' |
410 else raise TEST lthy4 |
411 else raise TEST lthy4 |
411 |
|
412 val _ = tracing ("bn_eqvts\n" ^ cat_lines (map @{make_string} bn_eqvt)) |
|
413 val _ = tracing ("fv_eqvts\n" ^ cat_lines (map @{make_string} fv_eqvt)) |
|
414 val _ = tracing ("alpha_eqvts\n" ^ cat_lines (map @{make_string} alpha_eqvt)) |
|
415 |
412 |
416 val _ = |
413 val _ = |
417 if get_STEPS lthy > 9 |
414 if get_STEPS lthy > 9 |
418 then true else raise TEST lthy4 |
415 then true else raise TEST lthy4 |
419 |
416 |