equal
deleted
inserted
replaced
693 val perm_app = thm "Nominal.pt_fun_app_eq"; |
693 val perm_app = thm "Nominal.pt_fun_app_eq"; |
694 val at_fresh = thm "Nominal.at_fresh"; |
694 val at_fresh = thm "Nominal.at_fresh"; |
695 val at_fresh_ineq = thm "Nominal.at_fresh_ineq"; |
695 val at_fresh_ineq = thm "Nominal.at_fresh_ineq"; |
696 val at_calc = thms "Nominal.at_calc"; |
696 val at_calc = thms "Nominal.at_calc"; |
697 val at_swap_simps = thms "Nominal.at_swap_simps"; |
697 val at_swap_simps = thms "Nominal.at_swap_simps"; |
698 val swap_simp_a = thm "swap_simp_a"; |
|
699 val swap_simp_b = thm "swap_simp_b"; |
|
700 val at_supp = thm "Nominal.at_supp"; |
698 val at_supp = thm "Nominal.at_supp"; |
701 val dj_supp = thm "Nominal.dj_supp"; |
699 val dj_supp = thm "Nominal.dj_supp"; |
702 val fresh_left_ineq = thm "Nominal.pt_fresh_left_ineq"; |
700 val fresh_left_ineq = thm "Nominal.pt_fresh_left_ineq"; |
703 val fresh_left = thm "Nominal.pt_fresh_left"; |
701 val fresh_left = thm "Nominal.pt_fresh_left"; |
704 val fresh_right_ineq = thm "Nominal.pt_fresh_right_ineq"; |
702 val fresh_right_ineq = thm "Nominal.pt_fresh_right_ineq"; |