771 let val thms1 = inst_at [at_fresh] |
771 let val thms1 = inst_at [at_fresh] |
772 val thms2 = inst_dj [at_fresh_ineq] |
772 val thms2 = inst_dj [at_fresh_ineq] |
773 in [(("fresh_atm", thms1 @ thms2),[])] end |
773 in [(("fresh_atm", thms1 @ thms2),[])] end |
774 ||>> PureThy.add_thmss |
774 ||>> PureThy.add_thmss |
775 let val thms1 = List.concat (List.concat perm_defs) |
775 let val thms1 = List.concat (List.concat perm_defs) |
776 val thms2 = List.concat prm_eqs |
776 in [(("calc_atm", (inst_at at_calc) @ thms1),[])] end |
777 val thms3 = List.concat swap_eqs |
|
778 in [(("calc_atm", (inst_at at_calc) @ thms1 @ thms2 @ thms3 ),[])] end |
|
779 ||>> PureThy.add_thmss |
777 ||>> PureThy.add_thmss |
780 let val thms1 = inst_pt_at [abs_fun_pi] |
778 let val thms1 = inst_pt_at [abs_fun_pi] |
781 and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq] |
779 and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq] |
782 in [(("abs_perm", thms1 @ thms2),[])] end |
780 in [(("abs_perm", thms1 @ thms2),[])] end |
783 ||>> PureThy.add_thmss |
781 ||>> PureThy.add_thmss |