Nominal/Ex/Ex2.thy
changeset 2104 2205b572bc9b
parent 2082 0854af516f14
child 2105 e25b0fff0dd2
equal deleted inserted replaced
2103:e08e3c29dbc0 2104:2205b572bc9b
    26 thm trm_pat.induct
    26 thm trm_pat.induct
    27 thm trm_pat.distinct
    27 thm trm_pat.distinct
    28 thm trm_pat.fv[simplified trm_pat.supp(1-2)]
    28 thm trm_pat.fv[simplified trm_pat.supp(1-2)]
    29 
    29 
    30 declare permute_trm_raw_permute_pat_raw.simps[eqvt]
    30 declare permute_trm_raw_permute_pat_raw.simps[eqvt]
    31 declare alpha_gen_eqvt[eqvt]
       
    32 
    31 
    33 equivariance alpha_trm_raw
    32 equivariance alpha_trm_raw
    34 
    33 
    35 
    34 
    36 end
    35 end