src/HOL/Nominal/nominal_atoms.ML
changeset 22609 40ade470e319
parent 22557 6775c71f1da0
child 22610 c8b5133045f3
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Fri Apr 06 01:26:30 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Apr 07 11:05:25 2007 +0200
     1.3 @@ -694,6 +694,8 @@
     1.4         val at_fresh            = thm "Nominal.at_fresh";
     1.5         val at_fresh_ineq       = thm "Nominal.at_fresh_ineq";
     1.6         val at_calc             = thms "Nominal.at_calc";
     1.7 +       val swap_simp_a         = thm "swap_simp_a";
     1.8 +       val swap_simp_b         = thm "swap_simp_b";
     1.9         val at_supp             = thm "Nominal.at_supp";
    1.10         val dj_supp             = thm "Nominal.dj_supp";
    1.11         val fresh_left_ineq     = thm "Nominal.pt_fresh_left_ineq";
    1.12 @@ -800,6 +802,8 @@
    1.13              ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
    1.14              ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
    1.15              ||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
    1.16 +            ||>> PureThy.add_thmss [(("swap_simp_a", inst_at [swap_simp_a]),[])]	 
    1.17 +            ||>> PureThy.add_thmss [(("swap_simp_b", inst_at [swap_simp_b]),[])]
    1.18              ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[NominalThmDecls.eqvt_add])] 
    1.19              ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_add])]
    1.20              ||>> PureThy.add_thmss