Nominal/Nominal2_Eqvt.thy
changeset 1331 0f329449e304
parent 1326 4bc9278a808d
child 1423 d59f851926c5
equal deleted inserted replaced
1330:88d2d4beb9e0 1331:0f329449e304
   249 
   249 
   250   (* sets *)
   250   (* sets *)
   251   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
   251   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
   252   Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt
   252   Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt
   253 
   253 
   254   atom_eqvt
   254   atom_eqvt add_perm_eqvt
   255 
   255 
   256 thm eqvts
   256 thm eqvts
   257 thm eqvts_raw
   257 thm eqvts_raw
   258 
   258 
   259 text {* helper lemmas for the eqvt_tac *}
   259 text {* helper lemmas for the eqvt_tac *}