src/HOL/Nominal/nominal_atoms.ML
changeset 22785 fab155c8ce46
parent 22768 d41fe3416f52
child 22786 d8d7a53ffb63
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Apr 24 15:19:33 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Apr 24 16:44:11 2007 +0200
     1.3 @@ -716,8 +716,9 @@
     1.4         val pt_rev_pi           = thm "Nominal.pt_rev_pi";
     1.5         val at_exists_fresh     = thm "Nominal.at_exists_fresh";
     1.6         val at_exists_fresh'    = thm "Nominal.at_exists_fresh'";
     1.7 -
     1.8 -
     1.9 +       val fresh_perm_app_ineq = thm "pt_fresh_perm_app_ineq";
    1.10 +       val fresh_perm_app      = thm "pt_fresh_perm_app";	
    1.11 +  
    1.12         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
    1.13         (* types; this allows for example to use abs_perm (which is a      *)
    1.14         (* collection of theorems) instead of thm abs_fun_pi with explicit *)
    1.15 @@ -858,7 +859,11 @@
    1.16              ||>> PureThy.add_thmss
    1.17  	      let val thms1 = inst_pt_at [fresh_aux]
    1.18  		  and thms2 = inst_pt_pt_at_cp_dj [fresh_aux_ineq]
    1.19 -	      in [(("fresh_aux", thms1 @ thms2),[])] end
    1.20 +	      in [(("fresh_aux", thms1 @ thms2),[])] end  
    1.21 +            ||>> PureThy.add_thmss
    1.22 +	      let val thms1 = inst_pt_at [fresh_perm_app]
    1.23 +		  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq]
    1.24 +	      in [(("fresh_perm_app", thms1 @ thms2),[])] end
    1.25              ||>> PureThy.add_thmss [(("fin_supp",fs_axs),[])]
    1.26  	   end;
    1.27