src/HOL/HOL.thy
changeset 47389 e8552cba702d
parent 46973 d68798000e46
child 47657 1ba213363d0c