454 val q_fv = map (lift_thm qtys lthy15) fv_def; |
454 val q_fv = map (lift_thm qtys lthy15) fv_def; |
455 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
455 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
456 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; |
456 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; |
457 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
457 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
458 val _ = tracing "Lifting eq-iff"; |
458 val _ = tracing "Lifting eq-iff"; |
459 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) alpha_eq_iff |
459 val _ = map tracing (map PolyML.makestring alpha_eq_iff); |
460 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas}) eq_iff_unfolded1 |
460 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff |
461 val q_eq_iff_pre1 = map (lift_thm qtys lthy17) eq_iff_unfolded2; |
461 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0 |
|
462 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1 |
|
463 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2; |
|
464 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0 |
462 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1 |
465 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1 |
463 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2 |
466 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2 |
464 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
467 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
465 val q_dis = map (lift_thm qtys lthy18) rel_dists; |
468 val q_dis = map (lift_thm qtys lthy18) rel_dists; |
466 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
469 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |