Another fine point that showed up in Isabelle2012-RC2 last Monday: lemma "1 + 1 = 2" by simp -- works value "1 + 1" -- "(1∷'a) + (1∷'a)" value "[1] = [2]" -- "equal_class.equal (1∷'a) ((1∷'a) + (1∷'a))" This is all correct, but maybe a bit unexpected for users. Makarius