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_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
