src/HOL/Nominal/nominal_atoms.ML
changeset 22786 d8d7a53ffb63
parent 22785 fab155c8ce46
child 22794 d0f483fd57dd
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Apr 24 16:44:11 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Apr 24 17:16:55 2007 +0200
     1.3 @@ -703,8 +703,6 @@
     1.4         val fresh_right         = thm "Nominal.pt_fresh_right";
     1.5         val fresh_bij_ineq      = thm "Nominal.pt_fresh_bij_ineq";
     1.6         val fresh_bij           = thm "Nominal.pt_fresh_bij";
     1.7 -       val fresh_aux_ineq      = thm "Nominal.pt_fresh_aux_ineq";
     1.8 -       val fresh_aux           = thm "Nominal.pt_fresh_aux";
     1.9         val fresh_eqvt          = thm "Nominal.pt_fresh_eqvt";
    1.10         val fresh_eqvt_ineq     = thm "Nominal.pt_fresh_eqvt_ineq";
    1.11         val set_diff_eqvt       = thm "Nominal.pt_set_diff_eqvt";
    1.12 @@ -716,9 +714,10 @@
    1.13         val pt_rev_pi           = thm "Nominal.pt_rev_pi";
    1.14         val at_exists_fresh     = thm "Nominal.at_exists_fresh";
    1.15         val at_exists_fresh'    = thm "Nominal.at_exists_fresh'";
    1.16 -       val fresh_perm_app_ineq = thm "pt_fresh_perm_app_ineq";
    1.17 -       val fresh_perm_app      = thm "pt_fresh_perm_app";	
    1.18 -  
    1.19 +       val fresh_perm_app_ineq = thm "Nominal.pt_fresh_perm_app_ineq";
    1.20 +       val fresh_perm_app      = thm "Nominal.pt_fresh_perm_app";	
    1.21 +       val fresh_aux           = thm "Nominal.pt_fresh_aux";  
    1.22 +
    1.23         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
    1.24         (* types; this allows for example to use abs_perm (which is a      *)
    1.25         (* collection of theorems) instead of thm abs_fun_pi with explicit *)
    1.26 @@ -858,12 +857,12 @@
    1.27  	      in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
    1.28              ||>> PureThy.add_thmss
    1.29  	      let val thms1 = inst_pt_at [fresh_aux]
    1.30 -		  and thms2 = inst_pt_pt_at_cp_dj [fresh_aux_ineq]
    1.31 -	      in [(("fresh_aux", thms1 @ thms2),[])] end  
    1.32 +		  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
    1.33 +	      in  [(("fresh_aux", thms1 @ thms2),[])] end  
    1.34              ||>> PureThy.add_thmss
    1.35  	      let val thms1 = inst_pt_at [fresh_perm_app]
    1.36 -		  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq]
    1.37 -	      in [(("fresh_perm_app", thms1 @ thms2),[])] end
    1.38 +		  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
    1.39 +	      in  [(("fresh_perm_app", thms1 @ thms2),[])] end  
    1.40              ||>> PureThy.add_thmss [(("fin_supp",fs_axs),[])]
    1.41  	   end;
    1.42