src/HOL/Nominal/nominal_atoms.ML
changeset 19165 7dc4fc25de8d
parent 19139 af69e41eab5d
child 19275 3d10de7a8ca7
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Mar 01 10:27:48 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Mar 01 10:28:39 2006 +0100
     1.3 @@ -670,6 +670,7 @@
     1.4         val fresh_bij         = thm "nominal.pt_fresh_bij";
     1.5         val pt_pi_rev         = thm "nominal.pt_pi_rev";
     1.6         val pt_rev_pi         = thm "nominal.pt_rev_pi";
     1.7 +       val fresh_fun_eqvt    = thm "nominal.fresh_fun_equiv";
     1.8  
     1.9         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
    1.10         (* types; this allows for example to use abs_perm (which is a      *)
    1.11 @@ -776,6 +777,7 @@
    1.12  	      let val thms1 = inst_pt_at [fresh_bij]
    1.13  		  and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq]
    1.14  	      in [(("fresh_eqvt", thms1 @ thms2),[])] end
    1.15 +            ||>> PureThy.add_thmss [(("fresh_fun_eqvt",inst_pt_at [fresh_fun_eqvt]),[])]
    1.16  	   end;
    1.17  
    1.18      in NominalData.put (fold Symtab.update (map (rpair ()) full_ak_names)