src/HOL/Nominal/nominal_atoms.ML
changeset 28011 90074908db16
parent 27691 ce171cbd4b93
child 28083 103d9282a946
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Aug 27 01:27:33 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Aug 27 04:47:30 2008 +0200
     1.3 @@ -750,6 +750,8 @@
     1.4         val eq_eqvt             = @{thm "Nominal.pt_eq_eqvt"};
     1.5         val all_eqvt            = @{thm "Nominal.pt_all_eqvt"};
     1.6         val ex_eqvt             = @{thm "Nominal.pt_ex_eqvt"};
     1.7 +       val ex1_eqvt            = @{thm "Nominal.pt_ex1_eqvt"};
     1.8 +       val the_eqvt            = @{thm "Nominal.pt_the_eqvt"};
     1.9         val pt_pi_rev           = @{thm "Nominal.pt_pi_rev"};
    1.10         val pt_rev_pi           = @{thm "Nominal.pt_rev_pi"};
    1.11         val at_exists_fresh     = @{thm "Nominal.at_exists_fresh"};
    1.12 @@ -864,6 +866,8 @@
    1.13                  [(("all_eqvt", thms1 @ thms2), [NominalThmDecls.eqvt_force_add])]
    1.14                end
    1.15              ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])]
    1.16 +            ||>> PureThy.add_thmss [(("ex1_eqvt", inst_pt_at [ex1_eqvt]),[NominalThmDecls.eqvt_force_add])]
    1.17 +            ||>> PureThy.add_thmss [(("the_eqvt", inst_pt_at [the_eqvt]),[NominalThmDecls.eqvt_force_add])]
    1.18              ||>> PureThy.add_thmss 
    1.19                let val thms1 = inst_at [at_fresh]
    1.20                    val thms2 = inst_dj [at_fresh_ineq]