Replaced all but one occurrence of perm_simp_tac by perm_simproc_app, since perm_simp_tac now behaves in a different way (due to changes in swap_simps).

Rewrote code to use swap_simps rather than calc_atm (which tends to produce ridiculously large nested if-expressions).

moved HOL-Plain up;