push normalization further -- avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)

disable Find_Unused_Assms_Examples for now, to recover isatest sanity;

less massive arrow heads;

added explicit zoom box;