src/ZF/ex/Commutation.thy
2001-02-03 paulson 2001-02-03 commutation theory, ported by Sidi Ehmety