src/HOL/HOL.thy
changeset 22452 8a86fd2a1bf0
parent 22445 e4fd2d02391d
child 22467 c9357ef01168