src/HOL/HOL.thy
changeset 71751 abf3e80bd815
parent 71517 7807d828a061
child 71608 856c68ab6f13