equal
deleted
inserted
replaced
481 val q_fv = map (lift_thm qtys lthy15) fv_def; |
481 val q_fv = map (lift_thm qtys lthy15) fv_def; |
482 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
482 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
483 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; |
483 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; |
484 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
484 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
485 val _ = tracing "Lifting eq-iff"; |
485 val _ = tracing "Lifting eq-iff"; |
486 val _ = map tracing (map PolyML.makestring alpha_eq_iff); |
486 (* val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |
487 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff |
487 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff |
488 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0 |
488 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0 |
489 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1 |
489 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1 |
490 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2; |
490 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2; |
491 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0 |
491 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0 |