src/HOL/HOL.thy
changeset 47356 19fb95255ec9
parent 46973 d68798000e46
child 47657 1ba213363d0c