deleted remaining instances of swap_simp_a and swap_simp_b (obsolete now)
authorurbanc
Sat Apr 07 12:40:32 2007 +0200 (2007-04-07)
changeset 226110e008e3ddb1e
parent 22610 c8b5133045f3
child 22612 1f017e6a0395
deleted remaining instances of swap_simp_a and swap_simp_b (obsolete now)
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Apr 07 11:36:35 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Apr 07 12:40:32 2007 +0200
     1.3 @@ -695,8 +695,6 @@
     1.4         val at_fresh_ineq       = thm "Nominal.at_fresh_ineq";
     1.5         val at_calc             = thms "Nominal.at_calc";
     1.6         val at_swap_simps       = thms "Nominal.at_swap_simps";
     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";