src/HOL/HOL.thy
changeset 24245 4ffeb1dd048a
parent 24219 e558fe311376
child 24280 c9867bdf2424