src/HOL/Nominal/nominal_atoms.ML
changeset 19477 a95176d0f0dd
parent 19275 3d10de7a8ca7
child 19488 8bd2c840458e
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Apr 26 22:40:46 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Apr 27 01:41:30 2006 +0200
     1.3 @@ -520,6 +520,7 @@
     1.4         val cp_option_inst  = thm "cp_option_inst";
     1.5         val cp_noption_inst = thm "cp_noption_inst";
     1.6         val pt_perm_compose = thm "pt_perm_compose";
     1.7 +       
     1.8         val dj_pp_forget    = thm "dj_perm_perm_forget";
     1.9  
    1.10         (* shows that <aj> is an instance of cp_<ak>_<ai>  *)
    1.11 @@ -645,32 +646,32 @@
    1.12  
    1.13         (* abbreviations for some lemmas *)
    1.14         (*===============================*)
    1.15 -       val abs_fun_pi        = thm "nominal.abs_fun_pi";
    1.16 -       val abs_fun_pi_ineq   = thm "nominal.abs_fun_pi_ineq";
    1.17 -       val abs_fun_eq        = thm "nominal.abs_fun_eq";
    1.18 -       val dj_perm_forget    = thm "nominal.dj_perm_forget";
    1.19 -       val dj_pp_forget      = thm "nominal.dj_perm_perm_forget";
    1.20 -       val fresh_iff         = thm "nominal.fresh_abs_fun_iff";
    1.21 -       val fresh_iff_ineq    = thm "nominal.fresh_abs_fun_iff_ineq";
    1.22 -       val abs_fun_supp      = thm "nominal.abs_fun_supp";
    1.23 -       val abs_fun_supp_ineq = thm "nominal.abs_fun_supp_ineq";
    1.24 -       val pt_swap_bij       = thm "nominal.pt_swap_bij";
    1.25 -       val pt_fresh_fresh    = thm "nominal.pt_fresh_fresh";
    1.26 -       val pt_bij            = thm "nominal.pt_bij";
    1.27 -       val pt_perm_compose   = thm "nominal.pt_perm_compose";
    1.28 -       val pt_perm_compose'  = thm "nominal.pt_perm_compose'";
    1.29 -       val perm_app          = thm "nominal.pt_fun_app_eq";
    1.30 -       val at_fresh          = thm "nominal.at_fresh";
    1.31 -       val at_calc           = thms "nominal.at_calc";
    1.32 -       val at_supp           = thm "nominal.at_supp";
    1.33 -       val dj_supp           = thm "nominal.dj_supp";
    1.34 -       val fresh_left_ineq   = thm "nominal.pt_fresh_left_ineq";
    1.35 -       val fresh_left        = thm "nominal.pt_fresh_left";
    1.36 -       val fresh_bij_ineq    = thm "nominal.pt_fresh_bij_ineq";
    1.37 -       val fresh_bij         = thm "nominal.pt_fresh_bij";
    1.38 -       val pt_pi_rev         = thm "nominal.pt_pi_rev";
    1.39 -       val pt_rev_pi         = thm "nominal.pt_rev_pi";
    1.40 -       val fresh_fun_eqvt    = thm "nominal.fresh_fun_equiv";
    1.41 +       val abs_fun_pi          = thm "nominal.abs_fun_pi";
    1.42 +       val abs_fun_pi_ineq     = thm "nominal.abs_fun_pi_ineq";
    1.43 +       val abs_fun_eq          = thm "nominal.abs_fun_eq";
    1.44 +       val dj_perm_forget      = thm "nominal.dj_perm_forget";
    1.45 +       val dj_pp_forget        = thm "nominal.dj_perm_perm_forget";
    1.46 +       val fresh_iff           = thm "nominal.fresh_abs_fun_iff";
    1.47 +       val fresh_iff_ineq      = thm "nominal.fresh_abs_fun_iff_ineq";
    1.48 +       val abs_fun_supp        = thm "nominal.abs_fun_supp";
    1.49 +       val abs_fun_supp_ineq   = thm "nominal.abs_fun_supp_ineq";
    1.50 +       val pt_swap_bij         = thm "nominal.pt_swap_bij";
    1.51 +       val pt_fresh_fresh      = thm "nominal.pt_fresh_fresh";
    1.52 +       val pt_bij              = thm "nominal.pt_bij";
    1.53 +       val pt_perm_compose     = thm "nominal.pt_perm_compose";
    1.54 +       val pt_perm_compose'    = thm "nominal.pt_perm_compose'";
    1.55 +       val perm_app            = thm "nominal.pt_fun_app_eq";
    1.56 +       val at_fresh            = thm "nominal.at_fresh";
    1.57 +       val at_calc             = thms "nominal.at_calc";
    1.58 +       val at_supp             = thm "nominal.at_supp";
    1.59 +       val dj_supp             = thm "nominal.dj_supp";
    1.60 +       val fresh_left_ineq     = thm "nominal.pt_fresh_left_ineq";
    1.61 +       val fresh_left          = thm "nominal.pt_fresh_left";
    1.62 +       val fresh_bij_ineq      = thm "nominal.pt_fresh_bij_ineq";
    1.63 +       val fresh_bij           = thm "nominal.pt_fresh_bij";
    1.64 +       val pt_pi_rev           = thm "nominal.pt_pi_rev";
    1.65 +       val pt_rev_pi           = thm "nominal.pt_rev_pi";
    1.66 +       val fresh_fun_eqvt      = thm "nominal.fresh_fun_equiv";
    1.67  
    1.68         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
    1.69         (* types; this allows for example to use abs_perm (which is a      *)