# HG changeset patch # User urbanc # Date 1175346832 -7200 # Node ID 6775c71f1da0226114d2638efda5a5934618c8ab # Parent b067fdca022dfcbb6efdf7389d7a9993515183ce added pt_bij' to the collection perm_swap and also added abs_perm to the collection of equivariance lemmas diff -r b067fdca022d -r 6775c71f1da0 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Sat Mar 31 12:40:55 2007 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Sat Mar 31 15:13:52 2007 +0200 @@ -685,6 +685,7 @@ val abs_fun_supp = thm "Nominal.abs_fun_supp"; val abs_fun_supp_ineq = thm "Nominal.abs_fun_supp_ineq"; val pt_swap_bij = thm "Nominal.pt_swap_bij"; + val pt_swap_bij' = thm "Nominal.pt_swap_bij'"; val pt_fresh_fresh = thm "Nominal.pt_fresh_fresh"; val pt_bij = thm "Nominal.pt_bij"; val pt_perm_compose = thm "Nominal.pt_perm_compose"; @@ -783,7 +784,7 @@ thy32 |> PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])] ||>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])] - ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])] + ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])] ||>> PureThy.add_thmss let val thms1 = inst_pt_at [pt_pi_rev]; val thms2 = inst_pt_at [pt_rev_pi]; @@ -813,7 +814,7 @@ ||>> PureThy.add_thmss let val thms1 = inst_pt_at [abs_fun_pi] and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq] - in [(("abs_perm", thms1 @ thms2),[])] end + in [(("abs_perm", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end ||>> PureThy.add_thmss let val thms1 = inst_dj [dj_perm_forget] and thms2 = inst_dj [dj_pp_forget]