Nominal/Ex/Modules.thy
changeset 2120 2786ff1df475
parent 2105 e25b0fff0dd2
child 2436 3885dc2669f9
equal deleted inserted replaced
2119:238062c4c9f2 2120:2786ff1df475
    66 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts
    66 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts
    67 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct
    67 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct
    68 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)
    68 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)
    69 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)]
    69 thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)]
    70 
    70 
    71 equivariance alpha_trm_raw
       
    72 
    71 
    73 
    72 
    74 end
    73 end
    75 
    74 
    76 
    75