--- a/src/HOL/Nominal/nominal_atoms.ML Sat Apr 07 11:05:25 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Sat Apr 07 11:36:35 2007 +0200
@@ -694,6 +694,7 @@
val at_fresh = thm "Nominal.at_fresh";
val at_fresh_ineq = thm "Nominal.at_fresh_ineq";
val at_calc = thms "Nominal.at_calc";
+ val at_swap_simps = thms "Nominal.at_swap_simps";
val swap_simp_a = thm "swap_simp_a";
val swap_simp_b = thm "swap_simp_b";
val at_supp = thm "Nominal.at_supp";
@@ -787,6 +788,7 @@
|> 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] @ inst_pt_at [pt_swap_bij']),[])]
+ ||>> PureThy.add_thmss [(("swap_simps", inst_at at_swap_simps),[])]
||>> PureThy.add_thmss
let val thms1 = inst_pt_at [pt_pi_rev];
val thms2 = inst_pt_at [pt_rev_pi];
@@ -802,8 +804,6 @@
||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
- ||>> PureThy.add_thmss [(("swap_simp_a", inst_at [swap_simp_a]),[])]
- ||>> PureThy.add_thmss [(("swap_simp_b", inst_at [swap_simp_b]),[])]
||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[NominalThmDecls.eqvt_add])]
||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_add])]
||>> PureThy.add_thmss