Nominal/Nominal2_Eqvt.thy
changeset 2667 e3f8673085b1
parent 2663 54aade5d0fe6
child 2668 92c001d93225
equal deleted inserted replaced
2666:324a5d1289a3 2667:e3f8673085b1
    31   (* nominal *)
    31   (* nominal *)
    32   supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt 
    32   supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt 
    33   swap_eqvt flip_eqvt
    33   swap_eqvt flip_eqvt
    34 
    34 
    35   (* datatypes *)
    35   (* datatypes *)
    36   Pair_eqvt permute_list.simps 
    36   Pair_eqvt permute_list.simps permute_option.simps
    37 
    37 
    38   (* sets *)
    38   (* sets *)
    39   mem_eqvt empty_eqvt insert_eqvt set_eqvt
    39   mem_eqvt empty_eqvt insert_eqvt set_eqvt
    40 
    40 
    41   (* fsets *)
    41   (* fsets *)