src/HOL/Nominal/nominal_atoms.ML
changeset 26090 ec111fa4f8c5
parent 25919 8b1c0d434824
child 26337 44473c957672
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Mon Feb 18 02:10:55 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Feb 18 03:12:08 2008 +0100
     1.3 @@ -775,6 +775,7 @@
     1.4         val fresh_aux           = @{thm "Nominal.pt_fresh_aux"};  
     1.5         val pt_perm_supp_ineq   = @{thm "Nominal.pt_perm_supp_ineq"};
     1.6         val pt_perm_supp        = @{thm "Nominal.pt_perm_supp"};
     1.7 +       val subseteq_eqvt       = @{thm "Nominal.pt_subseteq_eqvt"};
     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 @@ -922,6 +923,9 @@
    1.12  	      let val thms1 = inst_pt_at [set_diff_eqvt]
    1.13  	      in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
    1.14              ||>> PureThy.add_thmss
    1.15 +	      let val thms1 = inst_pt_at [subseteq_eqvt]
    1.16 +	      in [(("subseteq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
    1.17 +            ||>> PureThy.add_thmss
    1.18  	      let val thms1 = inst_pt_at [fresh_aux]
    1.19  		  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
    1.20  	      in  [(("fresh_aux", thms1 @ thms2),[])] end