src/HOL/Nominal/nominal_atoms.ML
changeset 23158 749b6870b1a1
parent 23029 79ee75dc1e59
child 23894 1a4167d761ac
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Thu May 31 14:34:09 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu May 31 14:47:20 2007 +0200
     1.3 @@ -671,6 +671,8 @@
     1.4         val abs_fun_pi_ineq     = thm "Nominal.abs_fun_pi_ineq";
     1.5         val abs_fun_eq          = thm "Nominal.abs_fun_eq";
     1.6         val abs_fun_eq'         = thm "Nominal.abs_fun_eq'";
     1.7 +       val abs_fun_fresh       = thm "Nominal.abs_fun_fresh";
     1.8 +       val abs_fun_fresh'      = thm "Nominal.abs_fun_fresh'";
     1.9         val dj_perm_forget      = thm "Nominal.dj_perm_forget";
    1.10         val dj_pp_forget        = thm "Nominal.dj_perm_perm_forget";
    1.11         val fresh_iff           = thm "Nominal.fresh_abs_fun_iff";
    1.12 @@ -779,6 +781,8 @@
    1.13              thy32 
    1.14  	    |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
    1.15              ||>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])]
    1.16 +            ||>> PureThy.add_thmss [(("alpha_fresh", inst_pt_at [abs_fun_fresh]),[])]
    1.17 +            ||>> PureThy.add_thmss [(("alpha_fresh'", inst_pt_at [abs_fun_fresh']),[])]
    1.18              ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])]
    1.19              ||>> PureThy.add_thmss [(("swap_simps", inst_at at_swap_simps),[])]	 
    1.20              ||>> PureThy.add_thmss