Hi, by using sledgehammer, i get this: "z3": A prover error occurred: The SMT solver Z3 is not activated. To activate it, set the environment variable "Z3_NON_COMMERCIAL" to "yes", and restart the Isabelle system. See also "/cygdrive/c/Users/DRaco/Desktop/Work/Isabelle2013-1/contrib/z3-3.2/etc/settings" I went to settings and "Z3_NON_COMMERCIAL" was already set to "yes". What now? Thanx!