src/HOL/HOL.thy
changeset 42707 42d607a9ae65
parent 42477 52fa26b6c524
child 42795 66fcc9882784