769 ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[])] |
769 ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[])] |
770 ||>> PureThy.add_thmss |
770 ||>> PureThy.add_thmss |
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 [(("calc_atm", inst_at at_calc),[])] |
774 ||>> PureThy.add_thmss |
|
775 let val thms1 = List.concat (List.concat perm_defs) |
|
776 val thms2 = List.concat prm_eqs |
|
777 val thms3 = List.concat swap_eqs |
|
778 in [(("calc_atm", (inst_at at_calc) @ thms1 @ thms2 @ thms3 ),[])] end |
775 ||>> PureThy.add_thmss |
779 ||>> PureThy.add_thmss |
776 let val thms1 = inst_pt_at [abs_fun_pi] |
780 let val thms1 = inst_pt_at [abs_fun_pi] |
777 and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq] |
781 and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq] |
778 in [(("abs_perm", thms1 @ thms2),[])] end |
782 in [(("abs_perm", thms1 @ thms2),[])] end |
779 ||>> PureThy.add_thmss |
783 ||>> PureThy.add_thmss |