added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often
(*show_question_marks := false;*)
quick_and_dirty := true;
no_document use_thy "~~/src/HOL/Library/LaTeXsugar";
use_thy "Slides9"