Nominal/Ex/TestMorePerm.thy
changeset 2105 e25b0fff0dd2
parent 2104 2205b572bc9b
equal deleted inserted replaced
2104:2205b572bc9b 2105:e25b0fff0dd2
    24 
    24 
    25 thm permute_weird_raw.simps[no_vars]
    25 thm permute_weird_raw.simps[no_vars]
    26 thm alpha_weird_raw.intros[no_vars]
    26 thm alpha_weird_raw.intros[no_vars]
    27 thm fv_weird_raw.simps[no_vars]
    27 thm fv_weird_raw.simps[no_vars]
    28 
    28 
    29 declare permute_weird_raw.simps[eqvt]
       
    30 equivariance alpha_weird_raw
    29 equivariance alpha_weird_raw
    31 
    30 
    32 
    31 
    33 end
    32 end
    34 
    33