src/HOL/Nominal/nominal_atoms.ML
changeset 22794 d0f483fd57dd
parent 22786 d8d7a53ffb63
child 22846 fb79144af9a3
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Apr 25 17:50:48 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Apr 25 21:29:14 2007 +0200
     1.3 @@ -717,6 +717,8 @@
     1.4         val fresh_perm_app_ineq = thm "Nominal.pt_fresh_perm_app_ineq";
     1.5         val fresh_perm_app      = thm "Nominal.pt_fresh_perm_app";	
     1.6         val fresh_aux           = thm "Nominal.pt_fresh_aux";  
     1.7 +       val pt_perm_supp_ineq   = thm "Nominal.pt_perm_supp_ineq";
     1.8 +       val pt_perm_supp        = thm "Nominal.pt_perm_supp";
     1.9  
    1.10         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
    1.11         (* types; this allows for example to use abs_perm (which is a      *)
    1.12 @@ -862,7 +864,11 @@
    1.13              ||>> PureThy.add_thmss
    1.14  	      let val thms1 = inst_pt_at [fresh_perm_app]
    1.15  		  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
    1.16 -	      in  [(("fresh_perm_app", thms1 @ thms2),[])] end  
    1.17 +	      in  [(("fresh_perm_app", thms1 @ thms2),[])] end 
    1.18 +            ||>> PureThy.add_thmss
    1.19 +	      let val thms1 = inst_pt_at [pt_perm_supp]
    1.20 +		  and thms2 = inst_pt_pt_at_cp [pt_perm_supp_ineq] 
    1.21 +	      in  [(("supp_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end  
    1.22              ||>> PureThy.add_thmss [(("fin_supp",fs_axs),[])]
    1.23  	   end;
    1.24