src/HOL/HOL.thy
changeset 22172 e7d6cb237b5e
parent 22129 bb2203c93316
child 22218 30a8890d2967